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

[Derek Fawcus]

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