diff options
| author | Anton Trunov | 2020-05-13 11:23:05 +0300 |
|---|---|---|
| committer | Anton Trunov | 2020-05-13 11:54:45 +0300 |
| commit | 842502a7f0d37b2d159fa5ce90ef1e9ef604f4b7 (patch) | |
| tree | 9c4a12233b43922c9c9f5c638f53001a164818d4 /CONTRIBUTING.md | |
| parent | 67f0e9fd40dc2f7b30a8aec4c7efb032e61a001e (diff) | |
Clarify the documentation for merging PRs with overlays
Diffstat (limited to 'CONTRIBUTING.md')
| -rw-r--r-- | CONTRIBUTING.md | 4 |
1 files changed, 3 insertions, 1 deletions
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* |