Hi everyone

I can't remember if I shared this before, but here's a script to pull down a single PR into a new branch:

https://gist.github.com/stefanv/daa8fc7bae6dc002ad62

Usage:

git pr 1020

which creates a branch `pr/1020`. You can execute it a second time whenever you want to update the branch.

Stéfan