Add full pull request merge

[tuan-tu-tran]

in the current state of this, the pull request is merged on the remote but the local refs
must still be updated to reflect the merge on the remote and the remote merged branch must
be manually deleted e.g.:

merge.py -e PR_NUMBER
git checkout master
git pull
git branch -d local_branch
git push origin :remote_branch

We could add an option to the python script to handle all of this automatically.

But an easier (but dirtier) solution is to implement a bash script to do this:

• merge the pull request
• update local master
• delete all merged local branches on the remote (assuming that for each branch, there is a remote branch with the same name)
• delete all merged local branches