Merging PRs is done through a tool included with a clone of
$ python dev/merge-pr.py -u $GITHUB_USERNAME -P $GITHUB_ACCESS_TOKEN_OR_PASSWORD -p $PR_NUMBER
- If you have GitHub's 2FA turned you have to use an access token. See the GitHub docs on access tokens for how to set that up.
$PR_NUMBERis the pull request number you wish to merge.