diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-09 11:10:42 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-09 11:11:29 +0100 |
| commit | 8f56790546e74cadf62d91c7078853bcced11e37 (patch) | |
| tree | f2b746ffb81c92735bf96fe213993de1c9b371c1 /dev/ci/ci-bignums.sh | |
| parent | d9f79d97dbc503e149cba2df1b228a94d7ac970b (diff) | |
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.
Diffstat (limited to 'dev/ci/ci-bignums.sh')
| -rwxr-xr-x | dev/ci/ci-bignums.sh | 2 |
1 files changed, 1 insertions, 1 deletions
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 |