diff options
| author | coqbot-app[bot] | 2020-12-12 10:12:56 +0000 |
|---|---|---|
| committer | GitHub | 2020-12-12 10:12:56 +0000 |
| commit | 233629e8f6e40057a8caf7502047995427740ae8 (patch) | |
| tree | c7906708d8fabf20251b83502845715d4337d949 /dev/ci/user-overlays/README.md | |
| parent | fe72ccc708d345e126eb49230afc73db28c5f068 (diff) | |
| parent | 050a09a763ec25bafd90dfd7d7c08f971c4a2e3b (diff) | |
Merge PR #13603: [ci] function to declare projects
Reviewed-by: SkySkimmer
Ack-by: RalfJung
Ack-by: Zimmi48
Diffstat (limited to 'dev/ci/user-overlays/README.md')
| -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 |