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 <
dfa
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 or
