Re: github PR branches (was Re: CFBridging... Functions in Corebase)

[Ivan Vučica]

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 <address@hidden> 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
address@hidden
https://lists.gnu.org/mailman/listinfo/gnustep-dev