]> matita.cs.unibo.it Git - helm.git/commitdiff
now maketests uses matitaclean (but not in the right way)
authorEnrico Tassi <enrico.tassi@inria.fr>
Fri, 1 Jul 2005 14:55:19 +0000 (14:55 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Fri, 1 Jul 2005 14:55:19 +0000 (14:55 +0000)
tests are made in the stupid order, not in the needed one

helm/matita/scripts/do_tests.sh
helm/matita/scripts/profile_cvs.sh

index d2e7eec91cc34cc1d537f38a4a90cbbf14e3645e..3fd13e4cf418fafaa0eb2bca3194b436319f82f2 100755 (executable)
@@ -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"
index c3f19c03f56fdb8413d24ff34090baea67212474..f0cc00e8bf72d8b6460f36a829686b83802f7565 100755 (executable)
@@ -21,7 +21,7 @@ function compile {
   cd $2
   autoconf 1>/dev/null
   ./configure 1>/dev/null
-  make matitac matitac.opt updater 1>/dev/null
+  make matitac matitac.opt updater matitaclean 1>/dev/null
   sed "s/@@OWNER@@/profiler/" matita.conf.xml.sample | sed "s/@@PREFETCH@@/false/" > matita.conf.xml
   ./updater
   cd $OLD