On 2016-11-03 18:57, Lawrence Velázquez wrote: >> On Nov 3, 2016, at 1:46 PM, Rainer Müller <rai...@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 _______________________________________________ macports-dev mailing list macports-dev@lists.macosforge.org https://lists.macosforge.org/mailman/listinfo/macports-dev
