Instructions for working with PRs from forks

[bob-carpenter]

We are getting more pull requests from people outside of Stan-dev and there are no instructions on how to build the docs using a pull request from a fork. I'm sure it's just the usual, but I find it incredibly hard to figure this stuff out when all I want to do is review a pull request.

While someone's at it, they can fix the capitalization of "It" and not use code style for section headers. As is, the "It" looks like it's starting a new sentence, whereas it's really continuing a previous one and then the code style looks like what's being called. Just use descriptive headers.

[WardBrian]

Hi Bob --

I'm not sure where to write this down exactly, but here's what I do:

• For the longest time, I had this in my .gitconfig:

  [alias]
   pr = !"pr() { git fetch origin pull/$1/head:pr-$1; git checkout pr-$1; }; pr"

  Running, for example, git pr 935 inside a docs checkout would check out the branch from Add chapter on multiple imputation. #935. This is a nice git-only solution, but it gets more annoying if you want to write back to that branch (the correct incantation for doing so, for the sake of completeness is git push FORK_URL pr-NUMBER:FORK_BRANCH_NAME, so it would be git push git@github.com:abner-hb/add-mult-imp.git pr-935:master in the case of Add chapter on multiple imputation. #935)

• More recently, I've switched to using the github CLI gh: https://cli.github.com/. This provides the gh pr checkout command which does all of the above for you, checking out the branch and extra set up so that git push works without any extra machinery.

[bob-carpenter]

Thanks. I'm also not sure it goes with docs. This is just the usual problem for me that I'm almost always blocked by the dev ops. @mitzimorris sorted me out on this one, and I wrote down the steps I needed for the doc, so I'm OK going forward until things change.