How to do PRs

The Developer Guide provides the broad picture. This page provides more detailed guidance on development with git and GitHub. In particular, it provides guidance on how to set up a pull request (PR) that is easy to manage.

Create a new branch for each PR. The workflow should be:

git checkout master
git pull      # update from GitHub
git checkout -b issue-NNN-SUMMARY
# hack on code
git add ...
git commit ...
# hack more...
# ...
# push to a branch 
git push -u origin issue-NNN-SUMMARY
# use GitHub to create a PR from the branch