diff options
| author | Théo Zimmermann | 2020-05-14 15:31:11 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-05-14 15:31:11 +0200 |
| commit | 8dd5c47007817c104d57a449409a6b9c6f8ef12e (patch) | |
| tree | 416c8be9d63ea6b21ea66d7a3e1ff47cc132ba4b | |
| parent | 6f2b88649ec0c1e27befe7bcd2cdbec0ccee95d6 (diff) | |
| parent | 122ab27b2b4f02f370826a0a8ade78a0c0b2d416 (diff) | |
Merge PR #12312: Clarify the documentation for merging PRs with overlays
Reviewed-by: Zimmi48
| -rw-r--r-- | CONTRIBUTING.md | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 3582d18cf6..525ced7fee 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -828,7 +828,12 @@ 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 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* |