Properly merging pull requests

[Lawrence Velázquez]

> On Nov 3, 2016, at 2:16 PM, Rainer Müller <raimue at macports.org> wrote:
> 
> On 2016-11-03 18:57, Lawrence Velázquez wrote:
>>> On Nov 3, 2016, at 1:46 PM, Rainer Müller <raimue at macports.org> wrote:
>>> 
>>> I think the proper way to do it on GitHub would be as follows:
>>> When the pull request author checked the box for "Allow modifications by
>>> maintainers" [1], you can force-push your changes to the pull request
>>> branch, replacing the original commits. Then you can merge the pull
>>> request from the GitHub web interface.
>> 
>> GitHub will also automatically close the PR as "merged" if you push the
>> PR branch's changes to master from a local client. It's quite nice.
> 
> If I understand this correctly, the exact commits have to be on the pull
> request branch for GitHub to recognize you want to close the PR. So I
> would have to push them first to the pull request branch and then to master.

Yeah, I think that's right. That means that rebasing from the command
line is not feasible for most PRs because the contributors' branch is
unlikely to be based on the absolute latest master. So I think the
process you mentioned (push to collaborator's branch, rebase from the
web) might become our standard operating procedure.

vq