Next bug fix

262be4d3 · Heiko Becker · b1ba3071 · 262be4d3
Commit 262be4d3 authored Apr 18, 2018 by Heiko Becker
Hide whitespace changes
Inline Side-by-side

Showing with 1 addition and 1 deletion

scripts/ci-hol4.sh scripts/ci-hol4.sh +1 -1

No files found.
--- a/scripts/ci-hol4.sh
+++ b/scripts/ci-hol4.sh
@@ -4,7 +4,7 @@ cd ./hol4
 #Run configure script to check the versions
 RET=./configure_hol.sh

-if [[ $RET -eq 1]]
+if [ $RET -eq 1 ];
 then
   echo "Updating HOL4 to the latest state specified in HOLCOMMIT"
   ./configure_hol.sh --init