diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-12-26 12:51:37 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-12-26 12:51:37 +0100 |
| commit | a270f1fef1476b324844e931cbb8195273e2d0f0 (patch) | |
| tree | 9c63cd729c92589bc40a8dc4dd0499f2683e30bb /dev/ci/user-overlays/README.md | |
| parent | b9f72bf53c831bd93d28760eefdab9ad8ffdac03 (diff) | |
Fix overlay selection for Circle CI.
Diffstat (limited to 'dev/ci/user-overlays/README.md')
| -rw-r--r-- | dev/ci/user-overlays/README.md | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md index 9146d3d52..9f0377cee 100644 --- a/dev/ci/user-overlays/README.md +++ b/dev/ci/user-overlays/README.md @@ -7,8 +7,10 @@ The name of your overlay file should be of the form `five_digit_PR_number-GitHub Example: `00669-maximedenes-ssr-merge.sh` containing ``` -if [ "$TRAVIS_PULL_REQUEST" = "669" ] || [ "$TRAVIS_BRANCH" = "ssr-merge" ]; then +if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then mathcomp_CI_BRANCH=ssr-merge mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git fi ``` + +(`CI_PULL_REQUEST` and `CI_BRANCH` are set in [`ci-common.sh`](/dev/ci/ci-common.sh)) |