25 Oct
2017
25 Oct
'17
7:38 p.m.
On Wed, Oct 25, 2017 at 12:05 PM, Daniel James via Boost
You can fetch the pull request from your own repo, see:
https://help.github.com/articles/checking-out-pull-requests-locally/#modifyi...
Or if you want to configure git to fetch all pull requests (including closed pull requests), do this in your repo:
git config --add remote.origin.fetch "+refs/pull/*/head:refs/remotes/origin/pr/*"
Very nice, I did not know this! This is a great opportunity to reiterate that learning git is a life-long process, it seems like there is always something new to be learned even if you've been using git for years.