Properly merging pull requests

[Rainer Müller]

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.

Rainer