PR Workflow

We use the bors-ng bot to merge PRs. In short, when someone replies bors r+, your PR has been scheduled for final tests and will be automatically merged. If a maintainer replies bors delegate+, then you have been granted the authority to merge your own PR (usually this will happen if there are some trivial changes required). For a full list of bors commands, see the bors documentation.