From f72df6adb6d0f473845f97912d8a8429471430b2 Mon Sep 17 00:00:00 2001
From: Heiko Becker <hbecker@mpi-sws.org>
Date: Thu, 17 Jun 2021 11:03:45 +0000
Subject: [PATCH] Update regressiontests.sh to disable binary tests
---
scripts/regressiontests.sh | 20 ++++++++++----------
1 file changed, 10 insertions(+), 10 deletions(-)
diff --git a/scripts/regressiontests.sh b/scripts/regressiontests.sh
index 3672b86e..bd04ebfd 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
--
GitLab