Properly merging pull requests

[Lawrence Velázquez]

> 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.

vq