awaiting-CI, bors, and the PR #queue

Stream: general

[Johan Commelin]

There are two new labels that we started using recently: awaiting-CI and ready-for-bors.

• awaiting-CI means that CI is currently running on this PR, and it should not be merged before CI is done
• ready-for-bors is a label that a maintainer might add to indicate: for reasons, probably because CI is still running, this can't be merged now. But other than that, it is ready to go. This means that other maintainers (or the author, after a bors d+) can merge the PR as soon as CI is ready.

PR #9478 (which is on the queue) updates the bors configuration. After that PR, bors will refuse to merge a PR with the awaiting-CI label.

Finally, the link #queue now points to a list of open PRs that are awaiting-review, but not awaiting-CI, not blocked-by-another-PR, do not have merge-conflict and no status failure.
If you want maintainers to look at your PR, make sure that it shows up on that list!