Merging github pull requests

[Dan Debrunner <dj...@debrunners.com>]

[This is for committers]

Very easy & way cool!

I just merged this pull request:

https://github.com/apache/incubator-quarks/pull/3


I'm using a separate clean repo clone that I do not do development on:

# This is one-time setup
git clone https://git-wip-us.apache.org/repos/asf/incubator-quarks.git 

cd incubator-quarks 

git remote add mirror git@github.com:apache/incubator-quarks.git 



Then to merge a pull request:

# This creates a new local branch pr-3 (any name could be used) from pull request 3
git fetch mirror pull/3/head:pr-3

# Merge and then push to master
git merge pr-3
git push origin master 


# pr-3 is only a temp branch, no need to push to origin (asf)
git branch -d pr-3

Now, doing this also automatically closed the pull request!

Note on subsequent merges before you merge to master you should ensure it is up to date using git pull.

Have fun!
Dan.