How to merge pull requests (Admin documentation)
This documentation is meant for github.com/collective admins.
Merging pull requests via the github.com web interface is very convenient, but sometimes merge conflicts cannot be resolved automatically. Then you have to do it manually, like so:
1. Clone github.com/collective, if not done already (or be sure to operate on the master branch):
$ git clone firstname.lastname@example.org:collective/collective.github.com.git
2. Add the remote repository from which the pull request comes from and fetch it:
$ git remote add thet git://github.com/thet/collective.github.com.git $ git fetch thet
- Merge it and resolve the merge conflicts manually:
$ git merge thet/master $ vim permissions.cfg
Commit and push it back.
$ git commit permissions.cfg -m"merge with thet/master" $ git push
For more Information see the Github help page on this topic.