Technically, "pull/ID/head" is a reference (a 'ref') in the remote repo, not a branch name.
And for clarification to other readers, BRANCHNAME is user-specified (i.e. it specifies which local branch name should this remote ref be pulled into). :) On Wed, Aug 23, 2017 at 9:48 PM Derek Fawcus < dfawcus+lists-gnustep-...@employees.org> wrote: > On the question of how to add to a PR locally, have a look at this: > > https://help.github.com/articles/checking-out-pull-requests-locally/ > > Github (like the other git hosting services) make PRs available under a > well known branch name. So for a given 'ID', you'd do something like: > > git fetch origin pull/ID/head:BRANCHNAME > git checkout BRANCHNAME > > <hack ... hack; git add ...; git commit; possible git merge> > > Then either push to your own repo and open a new PR (if one does not have > commit access to the central repo), or just push to the central repo if > you have commit access to it. > > DF > > _______________________________________________ > Gnustep-dev mailing list > Gnustep-dev@gnu.org > https://lists.gnu.org/mailman/listinfo/gnustep-dev >
_______________________________________________ Gnustep-dev mailing list Gnustep-dev@gnu.org https://lists.gnu.org/mailman/listinfo/gnustep-dev
