From 9e0bd11e3e344cd86089dadf6f654ce685139802 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 19 Jul 2005 11:34:41 +0000
Subject: [PATCH] Used to left temporary file if something failed.

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

diff --git a/helm/matita/scripts/do_tests.sh b/helm/matita/scripts/do_tests.sh
index 970828a64..a195b9cf0 100755
--- a/helm/matita/scripts/do_tests.sh
+++ b/helm/matita/scripts/do_tests.sh
@@ -48,10 +48,10 @@ for T in $TODO; do
   RC=$?;
   if [ $RC = 0 ]; then
     printf "$OK\t`cat $TMP`\t$DO_TESTS_EXTRA\n"
+    rm $TMP
   else
     printf "$FAIL\t`cat $TMP`\t$DO_TESTS_EXTRA\n";
+    rm $TMP
     exit $RC
   fi
 done
-
-rm $TMP
-- 
2.39.2