Merging a Pull Request Locally
If a pull request won't merge automatically on GitHub, or if you'd rather have a look at the files on your own machine before you do the merge, there's an easy way to get that done. From your local clone, first list the refs at the origin:
git ls-remote origin
You should see something like this:
03072b7e1e1af130e300d649e2586193510a16e0 HEAD
03072b7e1e1af130e300d649e2586193510a16e0 refs/heads/master
908fc2c31a0954bff83ceb24caa1365c197f975a refs/pull/1/head
ead43099d8430d462adc4340ccf1c8f478745250 refs/pull/1/merge
19c60d339f86832bca5869e462b0b1d0c39a9e27 refs/tags/0.5.0
The refs/pull/1/head
contains the commits of pull request #1 (further pull requests will be sequentially numbered after that). Git won't fetch them by default, so you have to ask it to do so explicitly:
git fetch origin refs/pull/1/head
Now you can use the temporary FETCH_HEAD
label to diff against the pull-requested commits, log them, cherry-pick them, or just merge them outright. You have full access to all of the capabilities of Git on your local repo. Once you've merged the pull request, push your changes back up to your repo, and the pull request should be closed automatically. Magic!
Pro pro tip: FETCH_HEAD
gets overwritten the next time you fetch, so get your work done fairly soon after doing the fetch.