tweak PR process description
This commit is contained in:
parent
6728da5396
commit
1205c53946
1 changed files with 8 additions and 4 deletions
|
|
@ -19,10 +19,14 @@ When you get a review, please take care of the requested changes in new commits.
|
|||
existing commits. Generally avoid force-pushing. The only time you should force push is when there
|
||||
is a conflict with the master branch (in that case you should rebase across master, not merge), and
|
||||
all the way at the end of the review process when the reviewer tells you that the PR is done and you
|
||||
should squash the commits. If you are unsure how to use `git rebase` to squash commits, use `./miri
|
||||
squash` which automates the process but leaves little room for customization. (All this is to work
|
||||
around the fact that Github is quite bad at dealing with force pushes and does not support `git
|
||||
range-diff`. Maybe one day Github will be good at git and then life can become easier.)
|
||||
should squash the commits. (All this is to work around the fact that Github is quite bad at
|
||||
dealing with force pushes and does not support `git range-diff`.)
|
||||
|
||||
The recommended way to squash commits is to use `./miri squash`, which will make everything into a
|
||||
single commit. You will be asked for the commit message; please ensure it describes the entire PR.
|
||||
You can also use `git rebase` manually if you need more control (e.g. if there should be more than
|
||||
one commit at the end), but then please use `--keep-base` to ensure the PR remains based on the same
|
||||
upstream commit.
|
||||
|
||||
Most PRs bounce back and forth between the reviewer and the author several times, so it is good to
|
||||
keep track of who is expected to take the next step. We are using the `S-waiting-for-review` and
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue