Properly merging pull requests

[Lawrence Velázquez]

> On Nov 3, 2016, at 2:46 PM, Lawrence Velázquez <larryv at macports.org> wrote:
> 
> 
>> 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.

Actually I think I was mistaken about this. Rebasing onto master + fast-forward merging + pushing from the command line works fine, as long as you force-push your local changes to the PR branch first. It doesn't seem to matter where the PR branch was branched from; GitHub knows to isolate the changes that aren't in the base branch.

vq
Sent from my iPhone