...
A list of even more Cockroach jargon lives on this repository's wiki.
Merging
External contributors: you don't need to worry about this section. We'll merge your PR as soon as you've addressed all review feedback!
...
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.
...