Merging pull requests

A helpful tip when merging pull requests from outside contributors: use hub for convenience.

https://github.com/defunkt/hub

Follow the standalone instructions, and note the section on Windows if you’re using Git Bash. Among other things, it makes it easy to checkout someone’s pull request directly, without worrying about adding and fetching remote URLs yourself:

hub checkout https://github.com/AnalyticalGraphicsInc/cesium/pull/702

It does lots of other GitHub-oriented things too, such as transmogrifying an issue into a pull request.

I assume only those with commit access would be able to transmogrify issues? I would hope so. The problem is that if the pull request is not the correct fix for an issue, you have no way to “un-pull request” it; you would have to open a new issue.

Otherwise I set this up a couple of hours ago and it’s pretty slick so far.

http://developer.github.com/v3/issues/#edit-an-issue

Issue owners and users with push access can edit an issue.