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:
https://gist.github.com/piscisaureus/3342247
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.
--
http://mccormick.cx/
_______________________________________________
Pd-dev mailing list
Pd-dev@lists.iem.at
https://lists.puredata.info/listinfo/pd-dev
