(taking this off the github issue, since it's unrelated)
On 06/30/2017 09:40 AM, Dan Wilcox wrote:
(personally, I hardly ever use the merge button, because I want to test the merged code locally before publishing it)
You can add the submitters repo locally as a remote, fetch the remote branch, then checkout and test. If things are good, you hit the Github Merge button which handles all the rest. This has worked well for me in the past.
obviously there are a number of different workflows. this is what i like about git.
in any case: i, personally, find it tedious to have to switch back to the github webpage just to press the merge button when i can as well do a `git push`. (i've had a number of PRs that required some extra work after merge; doing it myself was way more energy-preserving than trying to get the committer fix the PR so it was 100% perfect)
merging locally and then doing `git push` is also one of the officially documented ways to *properly* merge a PR. (just go to a random PR where you have merge-priviliges; and click on "view command line instruction" besides the "Merge pull request" button). if this doesn't properly make the PR show up as "merged", then we've hit a bug at github and should report it (rather than adapt our workflows).
and then, there's always the chance that the PR doesn't actually apply cleanly any more (as was the case with PR#61), and applying it actually requires a re-write (as miller has done; and he was simply faster than me, who hadn't even noticed that the PR would no longer apply), thus making it impossible for github to automatically detect the merge.
i really think that this is an edge case, and that we really don't need any special action (to change whatever workflow one prefers).
gfma IOhannes