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-bignums.sh | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

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

diff --git a/dev/ci/ci-bignums.sh b/dev/ci/ci-bignums.sh
index c90e516ae9..0082919679 100755
--- a/dev/ci/ci-bignums.sh
+++ b/dev/ci/ci-bignums.sh
@@ -6,11 +6,11 @@ ci_dir="$(dirname "$0")"
 # Let's avoid to source ci-common twice in this case
 if [ -z "${CI_BUILD_DIR}" ];
 then
-    source ${ci_dir}/ci-common.sh
+    . "${ci_dir}/ci-common.sh"
 fi
 
-bignums_CI_DIR=${CI_BUILD_DIR}/Bignums
+bignums_CI_DIR="${CI_BUILD_DIR}/Bignums"
 
-git_checkout ${bignums_CI_BRANCH} ${bignums_CI_GITURL} ${bignums_CI_DIR}
+git_checkout "${bignums_CI_BRANCH}" "${bignums_CI_GITURL}" "${bignums_CI_DIR}"
 
-( cd ${bignums_CI_DIR} && make && make install)
+( cd "${bignums_CI_DIR}" && make && make install)
-- 
cgit v1.2.3