aboutsummaryrefslogtreecommitdiff
path: root/CONTRIBUTING.md
diff options
context:
space:
mode:
authorThéo Zimmermann2020-01-31 23:14:49 +0100
committerThéo Zimmermann2020-01-31 23:17:51 +0100
commit37070565e8b7bead15f5abda2c409f1ad2348fa1 (patch)
tree94726ba076f11a565346b12bc3a5ec162dca527d /CONTRIBUTING.md
parent40cf15b764e3c164a5913eb3347cc32684fbb77e (diff)
Clarify expectations for overlays in contributing guide and CI doc.
Contributors are *not* required to prepare all the patches by themselves. They can request help from project authors, who should be ready to take part in this. Also, finish replacing "development" by the more appropriate word "project".
Diffstat (limited to 'CONTRIBUTING.md')
-rw-r--r--CONTRIBUTING.md18
1 files changed, 14 insertions, 4 deletions
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 6a72b68af0..7656998a51 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -527,10 +527,20 @@ how you can anticipate the results of the CI before opening a PR.
Such a failure can indicate either a bug in your branch, or a breaking
change that you introduced voluntarily. All such breaking changes
should be properly documented in the [user changelog][user-changelog].
-Furthermore, a backward-compatible fix should be found, and this fix
-should be merged in the broken projects *before* your PR to the Coq
-repository can be. You can use the same documentation as above to
-learn about testing and fixing locally the broken libraries.
+Furthermore, a backward-compatible fix should be found, properly
+documented in the changelog when non-obvious, and this fix should be
+merged in the broken projects *before* your PR to the Coq repository
+can be.
+
+Note that once the breaking change is well understood, it should not
+feel like it is your role to fix every project that is affected: as
+long as reviewers have approved and are ready to integrate your
+breaking change, you are entitled to (politely) request project
+authors / maintainers to fix the breakage on their own, or help you
+fix it. Obviously, you should leave enough time for this to happen
+(you cannot expect a project maintainer to allocate time for this as
+soon as you request it) and you should be ready to listen to more
+feedback and reconsider the impact of your change.
#### Understanding reviewers' feedback ####