Johan Commelin (Oct 01 2021 at 08:12):
There are two new labels that we started using recently:
awaiting-CImeans that CI is currently running on this PR, and it should not be merged before CI is done
ready-for-borsis 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
Finally, the link #queue now points to a list of open PRs that are
awaiting-review, but 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!
Last updated: Aug 03 2023 at 10:10 UTC