The normal workflow is pretty simple: once a PR has received an LGTM, add a comment saying
bors r=<reviewer>[,<reviewer>]*. You can also use
bors r+ which will make your name show up as the reviewer in the git log (See the Bors docs for a full list of commands). Bors will typically wait till the CI on your PR turns green before attempting to compile the merge commit. If you're amending + force pushing a commit and bors r+ immediately, you might see it not wait. What we think happens is that bors looks towards the previous commit status instead of the newest one (because on webhook race behavior - this is all speculation). If you don't see the following message, you've done it too soon, and risk bors failing after the fact.
Waiting for PR status (Github check) to be set, probably by CI. Bors will automatically try to run when all required PR statuses are set.
Craig will take the approved PR (along with any other PRs approved at around the same time), merge them to
master (or whatever the PR's target branch is), and push that as the branch named
staging. This will trigger the TeamCity step for the merge candidate. If everything goes right and the build compiles, Craig will fast-forward
staging, and each of the PRs will be marked as merged. If at any time you need to cancel your in progress merge, type