TIL: Local checkout of a GitHub PR from another fork

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 https://github.com/username/frobnicator/pull/123)

• Create a local branch, let's say add-wibbles:

  git fetch origin pull/123/head:add-wibbles
  

  (Note that origin is 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 GitHub refs/pull namespace feature.