diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-05-22 11:09:58 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-05-24 16:44:40 +0200 |
| commit | c0dd7253faa83d1f3230e57071073df321a5e389 (patch) | |
| tree | e5406500c63a7087ed8de023e293814edbd74528 /dev/doc | |
| parent | e43b85c925c0c9c87e1dde69760d9ea343c5cfa8 (diff) | |
Improve merging and overlay documentations.
Clarification prompted by Jim Fehrle.
[ci skip]
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/MERGING.md | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md index a466124c1..14d30517c 100644 --- a/dev/doc/MERGING.md +++ b/dev/doc/MERGING.md @@ -43,8 +43,8 @@ A maintainer is expected to be reasonably reactive, but no specific timeframe is given for reviewing. (*) In case a component is touched in a trivial way (adding/removing one file in -a `Makefile`, etc), or by applying a systematic process (global renaming, -deprecationg propagation, etc) that has been reviewed globally, the assignee can +a `Makefile`, etc), or by applying a systematic refactoring process (global +renaming for instance) that has been reviewed globally, the assignee can say in a comment they think a review is not required and proceed with the merge. ## Merging @@ -92,7 +92,9 @@ messy history when there are conflicts. ### What to do if the PR has overlays If the PR breaks compatibility of some developments in CI, then the author must -have prepared overlays for these developments (see [`dev/ci/README.md`](/dev/ci/README.md)) +have prepared overlays for these developments (see +[`dev/ci/user-overlays/README.md`](/dev/ci/user-overlays/README.md) for +detailed explanations of what this is) and the PR must absolutely update the `CHANGES` file. There are two cases to consider: |