now maketests uses matitaclean (but not in the right way)

[helm.git] / helm / matita / scripts / do_tests.sh

diff --git a/helm/matita/scripts/do_tests.sh b/helm/matita/scripts/do_tests.sh
index d2e7eec91cc34cc1d537f38a4a90cbbf14e3645e..3fd13e4cf418fafaa0eb2bca3194b436319f82f2 100755 (executable)
--- a/helm/matita/scripts/do_tests.sh
+++ b/helm/matita/scripts/do_tests.sh
@@ -40,6 +40,7 @@ for T in $TODO; do
   if [ "$TWICE" = "1" ]; then
     $COMPILER $T 1>/dev/null 2>/dev/null
   fi
+  ./matitaclean $T 1>/dev/null 2>/dev/null
   /usr/bin/time --quiet -o $TMP -f "%E  %U  %S" $COMPILER $T >> $LOGFILE 2>&1
   if [ $? = 0 ]; then
     printf "$OK\t`cat $TMP`\t$DO_TESTS_EXTRA\n"