diff --git a/tests/test.sh b/tests/test.sh index 08a01ca..72cd941 100755 --- a/tests/test.sh +++ b/tests/test.sh @@ -50,8 +50,8 @@ if [ "$?" != "0" ]; then exit 1; fi ./tests/test_squareroot.sh $PROG $OUT if [ "$?" != "0" ]; then exit 1; fi -./tests/test_simpletheory.sh $PROG $OUT -if [ "$?" != "0" ]; then exit 1; fi +#./tests/test_simpletheory.sh $PROG $OUT +#if [ "$?" != "0" ]; then exit 1; fi #tests/test_trivial_atc.sh $PROG $OUT #if [ "$?" != "0" ]; then RC="1"; fi