From 214e1cb977f880a0790465ff81dcea7c9f74d7d2 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 1 Jul 2005 14:55:19 +0000 Subject: [PATCH] now maketests uses matitaclean (but not in the right way) tests are made in the stupid order, not in the needed one --- helm/matita/scripts/do_tests.sh | 1 + helm/matita/scripts/profile_cvs.sh | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) 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 -- 2.39.2