From 250502b01340ec6bedace85c6a2d4a4e57a107cf Mon Sep 17 00:00:00 2001
From: zapashcanon
Date: Wed, 21 Feb 2018 22:42:10 +0100
Subject: Improve shell scripts

---
 dev/ci/ci-common.sh | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'dev/ci/ci-common.sh')

diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index d7a356930e..189734a0bc 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -20,7 +20,8 @@ else
         export CI_PULL_REQUEST="$CIRCLE_PR_NUMBER"
         export CI_BRANCH="$CIRCLE_BRANCH"
     else # assume local
-        export CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)"
+        CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)"
+        export CI_BRANCH
     fi
     export COQBIN="$PWD/bin"
 fi
@@ -35,10 +36,10 @@ ls "$COQBIN"
 CI_BUILD_DIR="$PWD/_build_ci"
 
 # shellcheck source=ci-basic-overlay.sh
-source "${ci_dir}/ci-basic-overlay.sh"
+. "${ci_dir}/ci-basic-overlay.sh"
 for overlay in "${ci_dir}"/user-overlays/*.sh; do
     # shellcheck source=/dev/null
-    source "${overlay}"
+    . "${overlay}"
 done
 
 mathcomp_CI_DIR="${CI_BUILD_DIR}/math-comp"
@@ -68,7 +69,7 @@ git_checkout()
 
 checkout_mathcomp()
 {
-  git_checkout ${mathcomp_CI_BRANCH} ${mathcomp_CI_GITURL} ${1}
+  git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${1}"
 }
 
 make()
-- 
cgit v1.2.3