a thing i didn't know, but now do (thanks to #LiHaoyi!), is that you can fetch an unmerged pull request from github like git fetch origin pull/2752/head (where '2752' is github's identifier for the pull request), and then checkout or even merge FETCH_HEAD to play with it.
#github