diff options
| author | Emilio Jesus Gallego Arias | 2018-10-17 14:26:32 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-17 14:41:38 +0200 |
| commit | b33794516f4dd10edcb06be49c0202a9e056c26e (patch) | |
| tree | 0fbf2eff7a667ff5c7f48d3a1c122041a8d26d94 /dev/ci/user-overlays | |
| parent | f111af975860b5f48bb792d718e4eb211f6fa57f (diff) | |
[ci] [doc] Notes about branch names.
I'd like to add this convention as it is very convenient for the
development of dev tools. Example, I can do `setup-coq-devs ltac
equations` and then get a fully composed tree. Similarly for preparing
overlays.
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`. |