diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-02-07 15:43:17 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-02-07 15:43:17 +0100 |
| commit | f12a980ad7136440210de1d275f909cc9dfb6fe4 (patch) | |
| tree | 1ad3ca4712af7a0a764dafba31eafea887fd021c | |
| parent | b1d56e48b2453814a5d2898688fbc7c5d29d32fa (diff) | |
ci-common: guess CI_BRANCH for local builds
| -rw-r--r-- | dev/ci/ci-common.sh | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 05fa33e97..d7a356930 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -19,6 +19,8 @@ else then export CI_PULL_REQUEST="$CIRCLE_PR_NUMBER" export CI_BRANCH="$CIRCLE_BRANCH" + else # assume local + export CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)" fi export COQBIN="$PWD/bin" fi |