diff options
| author | Gaëtan Gilbert | 2017-12-26 12:51:37 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2017-12-26 12:51:37 +0100 |
| commit | a270f1fef1476b324844e931cbb8195273e2d0f0 (patch) | |
| tree | 9c63cd729c92589bc40a8dc4dd0499f2683e30bb /dev/ci/ci-common.sh | |
| parent | b9f72bf53c831bd93d28760eefdab9ad8ffdac03 (diff) | |
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" |