diff options
| author | Maxime Dénès | 2017-12-27 10:19:51 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-12-27 10:19:51 +0100 |
| commit | 5cd3b9c6356ef3f35eddd3fa6d57375c92b09469 (patch) | |
| tree | 8af8c2fe8ab2db7a3899d5c7be4f51498fd75f02 /dev/ci/user-overlays/README.md | |
| parent | 37b198dc2ddf2f22e548a60a163607cfc6fbf4b5 (diff) | |
| parent | a270f1fef1476b324844e931cbb8195273e2d0f0 (diff) | |
Merge PR #6504: 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 9146d3d521..9f0377ceea 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)) |