.gitconfig: Add alias to merge GitHub pull request

Ref. https://help.github.com/articles/checking-out-pull-requests-locally

Closes #422.

.gitconfig

@@ -57,6 +57,18 @@
 	# List contributors with number of commits
 	contributors = shortlog --summary --numbered
 
+	# Merge GitHub pull request on top of the `master` branch
+	mpr = "!f() { \
+		if [ $(printf \"%s\" \"$1\" | grep '^[0-9]\\+$' > /dev/null; printf $?) -eq 0 ]; then \
+			git fetch origin refs/pull/$1/head:pr/$1 && \
+			git rebase master pr/$1 && \
+			git checkout master && \
+			git merge pr/$1 && \
+			git branch -D pr/$1 && \
+			git commit --amend -m \"$(git log -1 --pretty=%B)\n\nCloses #$1.\"; \
+		fi \
+	}; f"
+
 [apply]
 
 	# Detect whitespace errors when applying a patch