GitHub pull requests are tracked by a base and a head commit. Usually, base is master, and head is some feature branch. This allows the pull request on GitHub to pull in new changes to the commit as a discussion forms around it.
So in that sense, he is correct. There's no way to ensure that clicking the merge button is indeed merging what I think it's merging. Now that I type that, we could easily just include the latest SHA in the form and check that. Problem solved!
Alternatives to this are:
* Merge manually from the command line. This is typically what we do at GitHub.
* Request that people file pull requests with a SHA as the pull request head. This makes it impossible to update the pull request with future commits.
* Don't use pull requests.
Specifying the latest SHA as part of the merge would solve the trust problem. As other people have mentioned, allowing a final "review and fixup this patch" step before merging would also be useful for some workflows; this is what happens when you merge on the command line.
That leaves another major problem for us (the XS developers) which is that we actively encourage all development discussion and code review to be done on the mailing list where everyone involved sees it.
With GH pull requests this discussion gets fragmented into separate threads on the various pull requests.
Further, in my workflow, pulling in new changes to be committed into a pull request makes that pull request a new (version of) the original. See for example how Linux patches are discussed; you post an initial version, it gets discussed, you rework it, post a v2, and so on. At each point in time it is clear what exactly is being discussed.
Personally I have some other philosophical issues with GH that might be fun to discuss, get in touch by email if you're interested.
So GitHub pull requests point to the current head of a branch and not a specific commit? Tying a pull request to a specific commit (implicitly, not necessarily with new UI) seems like it would solve the problem.
That was my intention, I almost always merge from the command line, except for tiny & trivial pull requests, like documentation. Its hard to run the tests through the Github web UI.
For anyone that still cares, this has been tweaked. If you attempt to merge a pull request that has changed since you loaded the page, it'll require you to re-review the pull request.
