diff options
| author | Enrico Tassi | 2020-12-09 17:44:03 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2020-12-10 13:53:52 +0100 |
| commit | 3f4d6464ee2463291b5d6b65d8c40d6430c3c360 (patch) | |
| tree | 521ef6c30c7bf5a9eceaa0b75046d68f0326daf6 /dev/ci/user-overlays | |
| parent | 84e87cf712abed38699f58966abfa0b1c5bf5044 (diff) | |
[ci] simplify overlay scripts
Diffstat (limited to 'dev/ci/user-overlays')
| -rw-r--r-- | dev/ci/user-overlays/README.md | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md index 3f9ad5e878..14ee5e4199 100644 --- a/dev/ci/user-overlays/README.md +++ b/dev/ci/user-overlays/README.md @@ -21,14 +21,11 @@ and the branch name), then a `.sh` extension (`[0-9]{5}-[a-zA-Z0-9-_]+.sh`). Example: `13128-SkySkimmer-noinstance.sh` containing ``` -if [ "$CI_PULL_REQUEST" = "13128" ] || [ "$CI_BRANCH" = "noinstance" ]; then - - overlay elpi https://github.com/SkySkimmer/coq-elpi noinstance - -fi +overlay elpi https://github.com/SkySkimmer/coq-elpi noinstance 13128 ``` -(`CI_PULL_REQUEST` and `CI_BRANCH` are set in [`ci-common.sh`](../ci-common.sh)) +See [`ci-common.sh`](../ci-common.sh) for the detailed documentation of +the `overlay` function. ### Branching conventions |