Merge PR #8098: Update/improve two aspects of the merging process.

1 files changed, 34 insertions, 18 deletions

diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md
index 000f21c254..318562338d 100644
--- a/dev/doc/MERGING.md
+++ b/dev/doc/MERGING.md
@@ -6,19 +6,21 @@ This document describes how patches, submitted as pull requests (PRs) on the
 
 ## Code owners
 
-The [CODEOWNERS](../../.github/CODEOWNERS) file describes, for each part of the
-system, two owners. One is the principal maintainer of the component, the other
-is the secondary maintainer.
+The [CODEOWNERS](../../.github/CODEOWNERS) file defines owners for each part of
+the code. Sometime there is one principal maintainer and one or several
+secondary maintainer(s). Sometimes, it is a team of code owners and all of its
+members act as principal maintainers for the component.
 
 When a PR is submitted, GitHub will automatically ask the principal
-maintainer for a review. If the PR touches several parts, all the
-corresponding principal maintainers will be asked for a review.
+maintainer (or the code owner team) for a review. If the PR touches several
+parts, all the corresponding owners will be asked for a review.
 
 Maintainers are never assigned as reviewer on their own PRs.
 
-If a principal maintainer submits a PR that changes the component they own, they
-must assign the secondary maintainer as reviewer. They should also do it if they
-know they are not available to do the review.
+If a principal maintainer submits a PR or is a co-author of a PR that is
+submitted and this PR changes the component they own, they must request a
+review from a secondary maintainer. They can also delegate the review if they
+know they are not available to do it.
 
 ## Reviewing
 
@@ -35,17 +37,29 @@ When maintainers receive a review request, they are expected to:
   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
-same component, except if it would lead to a maintainer reviewing their own
-patch.
+When a PR received lots of comments or if the PR has not been opened for long
+and the assignee thinks that some other developers might want to comment,
+it is recommended that they announce their intention to merge and wait a full
+working day (or more if deemed useful) before the actual merge, as a sort of
+last call for comments.
+
+In all cases, maintainers can delegate reviews to the other maintainers,
+except if it would lead to a maintainer reviewing their own patch.
 
 A maintainer is expected to be reasonably reactive, but no specific timeframe is
 given for reviewing.
 
+When none of the maintainers have commented nor self-assigned a PR in a delay
+of five working days, any maintainer of another component who feels comfortable
+reviewing the PR can assign it to themselves. To prevent misunderstandings,
+maintainers should not hesitate to announce in advance when they shall be
+unavailable for more than five working days.
+
 (*) In case a component is touched in a trivial way (adding/removing one file in
 a `Makefile`, etc), or by applying a systematic refactoring process (global
 renaming for instance) that has been reviewed globally, the assignee can
-say in a comment they think a review is not required and proceed with the merge.
+say in a comment they think a review is not required from every code owner and
+proceed with the merge.
 
 ### Breaking changes
 
@@ -54,7 +68,8 @@ those external projects should have been prepared (cf. the relevant sub-section
 in the [CI README](../ci/README.md#Breaking-changes) and the PR can be tested
 with these fixes thanks to ["overlays"](../ci/user-overlays/README.md).
 
-Moreover the PR must absolutely update the [`CHANGES.md`](../../CHANGES.md) file.
+Moreover the PR must absolutely update the [`CHANGES.md`](../../CHANGES.md) or
+the [`dev/doc/changes.md`](changes.md) file.
 
 If overlays are missing, ask the author to prepare them and label the PR with
 the [needs: overlay](https://github.com/coq/coq/labels/needs%3A%20overlay) label.
@@ -78,9 +93,9 @@ put the approriate label. Otherwise, they are expected to merge the PR using the
 
 When CI has a few failures which look spurious, restarting the corresponding
 jobs is a good way of ensuring this was indeed the case.
-To restart a job on Travis, you should connect using your GitHub account;
-being part of the Coq organization on GitHub should give you the permission
-to do so.
+To restart a job on Travis or on AppVeyor, you should connect using your GitHub
+account; being part of the Coq organization on GitHub should give you the
+permission to do so.
 To restart a job on GitLab CI, you should sign into GitLab (this can be done
 using a GitHub account); if you are part of the
 [Coq organization on GitLab](https://gitlab.com/coq), you should see a "Retry"
@@ -93,9 +108,10 @@ When the PR has conflicts, the assignee can either:
 
 In both cases, CI should be run again.
 
-In some rare cases (e.g. the conflicts are in the `CHANGES.md` file), it is ok to fix
+In some rare cases (e.g. the conflicts are in the `CHANGES.md` file and the PR
+is not a candidate for backporting), 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.
+to `master` directly. DON'T USE the GitHub interface to fix these conflicts.
 
 To merge the PR proceed in the following way
 ```