Fetch GitHub Pull Requests Locally

It’s by no means a secret thing and Google will be the first to tell you, but by the off chance that someone hasn’t thought about it, here’s just the command how to do it.

git fetch origin pull/<id>/head:<branch>

<id> refers to the pull request id on GitHub
<branch> refers to a custom branch name of your choosing
Note: You can’t push back changes, but you can push them to your repository and create a new pull request.

Since we’re merging pull requests manually at SFML, it’s a command I’m using very frequently.