Commit 32d50f08 authored by Heiko Becker's avatar Heiko Becker

Fix another number bug in bash scripts

parent 262be4d3
...@@ -46,9 +46,9 @@ else ...@@ -46,9 +46,9 @@ else
if [[ "$CURR_HOL" = "$HOLCOMMIT" ]] if [[ "$CURR_HOL" = "$HOLCOMMIT" ]]
then then
echo "All set. HOL4 is on the correct commit." echo "All set. HOL4 is on the correct commit."
exit 0
else else
echo "Please make sure HOL4 uses the commit $HOLCOMMIT" echo "Please make sure HOL4 uses the commit $HOLCOMMIT"
echo "or consider running the script with the --init parameter." echo "or consider running the script with the --init parameter."
exit 1
fi fi
fi fi
...@@ -2,7 +2,8 @@ ...@@ -2,7 +2,8 @@
cd ./hol4 cd ./hol4
#Run configure script to check the versions #Run configure script to check the versions
RET=./configure_hol.sh ./configure_hol.sh
RET=$?
if [ $RET -eq 1 ]; if [ $RET -eq 1 ];
then then
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment