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