From f12a980ad7136440210de1d275f909cc9dfb6fe4 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 7 Feb 2018 15:43:17 +0100
Subject: ci-common: guess CI_BRANCH for local builds

---
 dev/ci/ci-common.sh | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'dev')

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
-- 
cgit v1.2.3