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/ci-common.sh | |
| parent | 37b198dc2ddf2f22e548a60a163607cfc6fbf4b5 (diff) | |
| parent | a270f1fef1476b324844e931cbb8195273e2d0f0 (diff) | |
Merge PR #6504: Fix overlay selection for Circle CI.
Diffstat (limited to 'dev/ci/ci-common.sh')
| -rw-r--r-- | dev/ci/ci-common.sh | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 23131c94c6..58c90ff11d 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -5,8 +5,17 @@ set -xe if [ -n "${GITLAB_CI}" ]; then export COQBIN=`pwd`/_install_ci/bin - export TRAVIS_BRANCH="$CI_COMMIT_REF_NAME" + export CI_BRANCH="$CI_COMMIT_REF_NAME" else + if [ -n "${TRAVIS}" ]; + then + export CI_PULL_REQUEST="$TRAVIS_PULL_REQUEST" + export CI_BRANCH="$TRAVIS_BRANCH" + elif [ -n "${CIRCLECI}" ]; + then + export CI_PULL_REQUEST="$CIRCLE_PR_NUMBER" + export CI_BRANCH="$CIRCLE_BRANCH" + fi export COQBIN=`pwd`/bin fi export PATH="$COQBIN:$PATH" |