ci/github-script/bot: skip PR checks when stale

It makes not much sense to run all the checks for PRs when we can
already tell they are stale beforehand. In particular this should avoid
creating ~3.3k temporary merge commits every day, for PRs that surely
won't have had any change.

The number of merge commits *could* play a role in the growing size of
the fork network. We'll have GitHub look into the metrics before and
after this change to see whether that is any improvement.

0 files changed, 0 insertions, 0 deletions