diff options
Diffstat (limited to 'dev/ci')
| -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 05fa33e972..d7a356930e 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 |