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 …