Versions Compared

Key

  • This line was added.
  • This line was removed.
  • Formatting was changed.

...

When your PR is ready to go, request a merge from our build bot Craig. Craig is a Bors merge bot, whose only job is to be gatekeeper to the repository. Add a comment on the PR of the form bors r=<reviewer>, replacing <reviewer> with the GitHub username of the person who gave you the LGTM. Once approved, your PR will be batched up with other PRs approved around the same time. Craig will try to build them as though they were merged to the target branch, and if successful, will merge them. This limits your exposure by ensuring you don't accidentally merge a commit with an obviously broken build or merge skew. (If Craig says "Permission denied", see the FAQ.)

We call merging locally and pushing to master the "nuclear option" or "god merging." It's not disabled, but you shouldn't do it unless the repo is on fire.

Congratulations on landing your first PR! It only gets easier from here.

...