fix

diff --git a/helm/matita/scripts/do_tests.sh b/helm/matita/scripts/do_tests.sh
index b8df5141895d7c96a59e1c6bb9e292431dc82b2c..1e27df81aa58ff4164bb9cb7db64c326b776dbba 100755 (executable)
--- 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