diff options
| author | Gaëtan Gilbert | 2018-10-30 21:44:25 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-10-30 21:44:25 +0100 |
| commit | d32301dde8071acc914286c675b9749e27f368d2 (patch) | |
| tree | cafcad3409648e40c44bcb8c3923885b5785157d /dev/ci/user-overlays | |
| parent | 0ac673e562c34245e4e48efc428d808e917be79b (diff) | |
| parent | b33794516f4dd10edcb06be49c0202a9e056c26e (diff) | |
Merge PR #8750: [ci] [doc] Notes about branch names.
Diffstat (limited to 'dev/ci/user-overlays')
| -rw-r--r-- | dev/ci/user-overlays/README.md | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md index 68afe7ee4a..7fb73e447d 100644 --- a/dev/ci/user-overlays/README.md +++ b/dev/ci/user-overlays/README.md @@ -33,3 +33,11 @@ fi ``` (`CI_PULL_REQUEST` and `CI_BRANCH` are set in [`ci-common.sh`](../ci-common.sh)) + +### Branching conventions + +We suggest you use the convention of identical branch names for the +Coq branch and the CI project branch used in the overlay. For example, +if your Coq PR is coming from the branch `more_efficient_tc`, and that +breaks `ltac2`, we suggest you create a `ltac2` overlay with a branch +named `more_efficient_tc`. |