Who clicks the “merge” button?
We have a convention that it’s usually the person assigned to the PR, who is usually the author. But in reality, if the PR has review approval and passes CI, anyone could click “merge” (or type bors merge).
We do also have a github label “DO NOT MERGE” which people can tag PRs with. (Absence of this label is not checked by CI, though it could be.)
Obviously, PRs marked as draft should not be merged. Draft PRs need not even be reviewed, unless it’s requested.
Rebasing vs. merging
We currently prefer rebasing PR branches onto master (followed by a push --force-with-lease) instead of merging master into the branch which would eventually be merged into master.
To squash or not to squash?
If your branch log reads like a historical account of your personal journey through developing the PR, with twists and all, please squash the branch.
If your branch log looks messy for other reasons, then just squash it all together so that our master branch can be tidy.
You will find that the less commits you have the easier rebasing will be.
If you can make your PR easier to review by splitting it into multiple commits, then please do so. In particular, it’s good to separate autogenerated stuff like nix files or golden test vectors into separate commits so that they don’t obscure the real changes.