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(-)

(limited to 'CONTRIBUTING.md')

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