From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 1 Jul 2005 14:55:19 +0000 (+0000)
Subject: now maketests uses matitaclean (but not in the right way)
X-Git-Tag: PRE_GETTER_STORAGE~57
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=214e1cb977f880a0790465ff81dcea7c9f74d7d2;p=helm.git

now maketests uses matitaclean (but not in the right way)
tests are made in the stupid order, not in the needed one
---

diff --git a/helm/matita/scripts/do_tests.sh b/helm/matita/scripts/do_tests.sh
index d2e7eec91..3fd13e4cf 100755
--- 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"
diff --git a/helm/matita/scripts/profile_cvs.sh b/helm/matita/scripts/profile_cvs.sh
index c3f19c03f..f0cc00e8b 100755
--- a/helm/matita/scripts/profile_cvs.sh
+++ b/helm/matita/scripts/profile_cvs.sh
@@ -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