diff --git a/scripts/regressiontests.sh b/scripts/regressiontests.sh index 3672b86ed8c8db356a71c6aed6456846c8873712..bd04ebfdc8ecb176bc1e16ccc4e02102352d76af 100755 --- a/scripts/regressiontests.sh +++ b/scripts/regressiontests.sh @@ -68,15 +68,15 @@ for fname in ./*.sml; do fi done -#Binary regression tests -for fname in ./*.txt; do - ../../hol4/binary/cake_checker $fname - if [ $? -eq 0 ] - then - echo "Successfully checked $fname"; - else - echo "Checking $fname has failed" - exit 1; - fi +#Binary regression tests; disabled +#for fname in ./*.txt; do +# ../../hol4/binary/cake_checker $fname +# if [ $? -eq 0 ] +# then +# echo "Successfully checked $fname"; +# else +# echo "Checking $fname has failed" +# exit 1; +# fi done