7 Jun
2018
7 Jun
'18
10:15 a.m.
On 07/06/18 15:05, IOhannes m zmoelnig wrote:
On 2018-06-07 03:00, Chris McCormick wrote:
It's possible to fetch all GitHub PRs to your local:
jeez, i didn't know that. this looks great.
I found this other hack too for fetching single PRs without adding a bunch of remotes:
$ cat ~/bin/git-fetch-github-pr #!/bin/sh
if [ "$1" = "" ] then echo "Usage: `basename $0` PR-ISSUE-ID [BRANCH]" else branch=${2-master} git fetch origin pull/$1/head:$branch fi
Cheers,
Chris.