aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-03-23 15:56:23 +0100
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-03-23 15:56:23 +0100
commit9236c0c40203f132eaa09436b0379d6dde23ddbe (patch)
tree902010b0edac3c1c4e20a318fccd718d25197ec1
parent4e3819425445c3236f6aca77e95f2ee854cf4417 (diff)
parentee62b9269beb78b12f1431816ea1acc0cd09130c (diff)
Merge PR #7052: More precise wording about the merge process.
-rw-r--r--dev/doc/MERGING.md24
1 files changed, 22 insertions, 2 deletions
diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md
index f1dddbd0e..71fc39608 100644
--- a/dev/doc/MERGING.md
+++ b/dev/doc/MERGING.md
@@ -30,8 +30,8 @@ When maintainers receive a review request, they are expected to:
* If they are the assignee, check if all reviewers approved the PR. If not,
regularly ping the author (if changes should be implemented) or the reviewers
(if reviews are missing). The assignee ensures that any requests for more
- discussion have been granted. When the discussion has converged and all
- reviewers have approved the PR, the assignee is expected to follow the merging
+ discussion have been granted. When the discussion has converged and ALL
+ REVIEWERS(*) have approved the PR, the assignee is expected to follow the merging
process described below.
In all cases, maintainers can delegate reviews to the other maintainer of the
@@ -41,6 +41,11 @@ patch.
A maintainer is expected to be reasonably reactive, but no specific timeframe is
given for reviewing.
+(*) In case a component is touched in a trivial way (adding/removing one file in
+a `Makefile`, etc), or by applying a systematic process (global renaming,
+deprecationg propagation, etc) that has been reviewed globally, the assignee can
+say in a comment they think a review is not required and proceed with the merge.
+
## Merging
Once all reviewers approved the PR, the assignee is expected to check that CI
@@ -49,6 +54,17 @@ documentation and test cases. If not, they should leave a comment on the PR and
put the approriate label. Otherwise, they are expected to merge the PR using the
[merge script](/dev/tools/merge-pr.sh).
+When the PR has conflicts, the assignee can either:
+- ask the author to rebase the branch, fixing the conflicts
+- warn the author that they are going to rebase the branch, and push to the
+ branch directly
+
+In both cases, CI should be run again.
+
+In some rare cases (e.g. the conflicts are in the CHANGES file), it is ok to fix
+the conflicts in the merge commit (following the same steps as below), and push
+to `master` directly. Don't use the GitHub interface to fix these conflicts.
+
The command to be used is:
```
$ dev/tools/merge-pr XXXX
@@ -56,3 +72,7 @@ $ dev/tools/merge-pr XXXX
where `XXXX` is the number of the PR to be merged. This operation should be followed by a push.
Maintainers MUST NOT merge their own patches.
+
+DON'T USE the GitHub interface for merging, since it will prevent the automated
+backport script from operating properly, generates bad commit messages, and a
+messy history when there are conflicts.