From 842502a7f0d37b2d159fa5ce90ef1e9ef604f4b7 Mon Sep 17 00:00:00 2001
From: Anton Trunov
Date: Wed, 13 May 2020 11:23:05 +0300
Subject: Clarify the documentation for merging PRs with overlays

---
 CONTRIBUTING.md | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 3582d18cf6..6794a296dc 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -828,7 +828,9 @@ organization, because of a limitation of GitHub).
 
   - the overlays that are backward-compatible (normally the case for
     overlays fixing Coq code) should have been merged *before* the PR
-    can be merged;
+    can be merged; it might be a good idea to ask the PR author to
+    remove the overlay information from the PR to get a fresh CI run
+    and ensure that all the overlays have been merged;
 
   - the overlays that are not backward-compatible (normally only the
     case for overlays fixing OCaml code) should be merged *just after*
-- 
cgit v1.2.3


From 122ab27b2b4f02f370826a0a8ade78a0c0b2d416 Mon Sep 17 00:00:00 2001
From: Anton Trunov
Date: Wed, 13 May 2020 13:14:17 +0300
Subject: Clarify the assignee's role in removing the overlay information

---
 CONTRIBUTING.md | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 6794a296dc..525ced7fee 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -830,7 +830,10 @@ organization, because of a limitation of GitHub).
     overlays fixing Coq code) should have been merged *before* the PR
     can be merged; it might be a good idea to ask the PR author to
     remove the overlay information from the PR to get a fresh CI run
-    and ensure that all the overlays have been merged;
+    and ensure that all the overlays have been merged; the PR assignee
+    may also push a commit removing the overlay information (in that
+    case the assignee is not considered a co-author, hence no need to
+    change the assignee)
 
   - the overlays that are not backward-compatible (normally only the
     case for overlays fixing OCaml code) should be merged *just after*
-- 
cgit v1.2.3