Today I learned that you can directly create a branch from a GitHub PR, created from another user's fork without explicitly adding that user's fork as a remote.
- Find out the PR's number (e.g. 123, given
Create a local branch, let's say
git fetch origin pull/123/head:add-wibbles
originis the remote the PR was made against, it doesn't refer to the user's fork)
Checkout out that branch
Fun fact: I learned this from ChatGPT
(after a bit of back and forth to make it understand what I was looking for)
and first thought it was hallucinating this solution,
because it did not mention the user's fork URL in any way.
But then found out you can indeed use this
refs/pull namespace feature.