git: pull PR into new branch

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