From fcbe774670d9ecc18b301de34934392621284cd9 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 13 Dec 2005 16:06:42 +0000
Subject: [PATCH] fix

---
 helm/matita/scripts/do_tests.sh | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/helm/matita/scripts/do_tests.sh b/helm/matita/scripts/do_tests.sh
index b8df51418..1e27df81a 100755
--- a/helm/matita/scripts/do_tests.sh
+++ b/helm/matita/scripts/do_tests.sh
@@ -41,11 +41,12 @@ if [ -z "$COMPILER" -o -z "$CLEANER" -o -z "$LOGFILE" -o -z "$EXPECTED" -o -z "$
   exit 1
 fi
 
-LOG=.__log
-DIFF=.__diff
 
 export TIMEFORMAT="%2lR %2lU %2lS"
 for T in $TODO; do
+  TT=`echo $T | sed s?/?.?`
+  LOG=__log_$TT
+  DIFF=__diff_$TT
   printf "$CLEANCOMPILER\t%-30s   " $T
   if [ "$TWICE" = "1" ]; then
     $CLEANER $T 1>/dev/null 2>/dev/null
@@ -65,13 +66,13 @@ for T in $TODO; do
      RC=$?
    fi
   fi
-  rm -f $LOG
   if [ $RC = 0 ]; then
     printf "$OK\t$TIMES\t$DO_TESTS_EXTRA\n"
   else
     printf "$FAIL\t$TIMES\t$DO_TESTS_EXTRA\n";
     cat $DIFF
   fi
-  rm -f $DIFF
+  #rm -f $LOG
+  #rm -f $DIFF
   exit $RC
 done
-- 
2.39.2