Merging PRs

Merging to the upstream git server

Many people, including project members, will submit changes as Github Pull Requests, but since github is acting as a read-only public mirror for the upstream private git server, merging requires a few extra steps.

If you just hit the green Merge button it github, it will look correct, but 30 mins later when the sync bots runs, it'll get overwritten. So instead, merge all PRs on the command-line, for example using the commands suggested by github in the View command line instructions clickable link at the bottom of the PR comment thread.

Squash merge

In order to keep the git commit history smaller, we prefer merging PRs as squash merges (this creates a single commit for the whole PR). So add --squash to the git merge command. For small PRs with only one or two commits, you can leave it un-squashed so that the contributor's commit remains and they get credit for the commit.