I like a clean, boring git history. I prefer this:
* 6ca186e Someone set us up the commit * f55bcf8 Initial commit
* 494c94e Merge pull request #1 from kormoc/pr_test |\ | * 6ca186e Someone set us up the commit |/ * f55bcf8 Initial commit
By default, github will preserve trivial merges when you use the “Merge pull request” button.
If you don’t want these trivial commits in your history, you have to pull (fetch/merge) locally. When someone creates a pull request for you, github sends you a handy email with a command you can cut and paste to perform the merge locally.
You can merge this Pull Request by running
git pull https://github.com/kormoc/pulltest pr_test
Or view, comment on, or merge it at:
git pull does an implicit
merge. If you merge locally and there are no conflicts, the trivial merge will be omitted.
You may miss the trivial commits because they include a reference to the pull request on github. I won’t. I might ask the patch submitter to refer to the pull request by name/link in their commit log message.
If you want to prevent anyone from pushing trivial merges, more work is required.
I now prefer what GitHub’s merge button does, namely: preserving the merge history for pull requests.