When do I open an issue?

• When there's something you want to document discussing about.
• When there's something that needs doing but you're not ready to hop into it immediately.

When do I open a Pull Request?

• When you have some changes in a local branch ready to be merged.
• When you're going to be working on something for some time and want to keep the process public.

If your PR is meant to resolve an issue mention it using it's number, like #7 references #5.

Either way, add a short description of what the PR is about. You can just copy or quote the one from the issue, if there's one.

I think my Pull Request is ready. What do I do next?

Mark it with the needs review label first. The reviewer might have some comments and/or feedback. Once you both agree the PR is ready she'll try to merge it using our merge script (tool/merge in the repo).

She's going to ask you to rebase the branch atop the current master if the merge script fails. It's ok to force push the rebased version. Nobody should start work off of something that's in review.

How do I use the merge script?

Checkout the branch you wish to merge into master and run ./tools/merge (this requires a Unix shell; try Git Bash if you're on Windows). If it fails ask the author of the branch to do a manual rebase on top of master and try it again. Once it succedes, push the newly merged master.

Never force a push to master.