My 2 cents:

* cherry-pick will always change commit hash and github won't see it as the
same commit as from original PR
* "Closed #10" syntax was designed to close Issues from commit messages. I
think if you do "Closes #10" for PR it will close a PR in the way it will
look like it was declined
* I think asking contributor to make required changes and then just merging
is a proper way to manage PRs. If you want to help contributor add comments
to bad lines or provide correct code snippets

On Thu, Nov 3, 2016 at 11:46 AM, Lawrence Velázquez <>

> > On Nov 3, 2016, at 2:16 PM, Rainer Müller <> wrote:
> >
> > On 2016-11-03 18:57, Lawrence Velázquez wrote:
> >>> On Nov 3, 2016, at 1:46 PM, Rainer Müller <> 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
> _______________________________________________
> macports-dev mailing list

With best regards, Ivan Larionov.
macports-dev mailing list

Reply via email to