diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-02-12 10:00:00 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-02-12 10:00:00 +0100 |
| commit | 8e048ebb124416448156dbfade1b7f826828e466 (patch) | |
| tree | 9718f600f4f5ff7ace211199c7139744ef8cafff /dev | |
| parent | 4fb4f1adf18648b4fb561986379e033b00423148 (diff) | |
| parent | f12a980ad7136440210de1d275f909cc9dfb6fe4 (diff) | |
Merge PR #6706: ci-common: guess CI_BRANCH for local builds
Diffstat (limited to 'dev')
| -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 |