From 8f56790546e74cadf62d91c7078853bcced11e37 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Thu, 9 Nov 2017 11:10:42 +0100
Subject: Fix ci-bignums.sh "missing ]" error.

It made the test always fail so ci-common was always sourced. It's not
quite idempotent as it adds COQBIN to PATH but it didn't lead to CI failure.
---
 dev/ci/ci-bignums.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/ci/ci-bignums.sh b/dev/ci/ci-bignums.sh
index ff5935d4c..d68674381 100755
--- a/dev/ci/ci-bignums.sh
+++ b/dev/ci/ci-bignums.sh
@@ -4,7 +4,7 @@ ci_dir="$(dirname "$0")"
 
 # This script could be included inside other ones
 # Let's avoid to source ci-common twice in this case
-if [ -z "${CI_BUILD_DIR}"];
+if [ -z "${CI_BUILD_DIR}" ];
 then
     source ${ci_dir}/ci-common.sh
 fi
-- 
cgit v1.2.3