diff options
| author | Anton Trunov | 2020-05-13 13:14:17 +0300 |
|---|---|---|
| committer | Anton Trunov | 2020-05-13 13:14:17 +0300 |
| commit | 122ab27b2b4f02f370826a0a8ade78a0c0b2d416 (patch) | |
| tree | 2c320359dc6a5aa033d1c25cbe1f0917cf7c1c12 | |
| parent | 842502a7f0d37b2d159fa5ce90ef1e9ef604f4b7 (diff) | |
Clarify the assignee's role in removing the overlay information
| -rw-r--r-- | CONTRIBUTING.md | 5 |
1 files changed, 4 insertions, 1 deletions
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* |