From 78229b5b53f947df657547e682c5365bbba9455b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 13 Dec 2005 18:54:42 +0000 Subject: [PATCH] one more try --- helm/matita/scripts/do_tests.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/matita/scripts/do_tests.sh b/helm/matita/scripts/do_tests.sh index 1e27df81a..b7500bf03 100755 --- a/helm/matita/scripts/do_tests.sh +++ b/helm/matita/scripts/do_tests.sh @@ -44,7 +44,7 @@ fi export TIMEFORMAT="%2lR %2lU %2lS" for T in $TODO; do - TT=`echo $T | sed s?/?.?` + TT=`echo $T | sed s?/?.?`.not_for_matita LOG=__log_$TT DIFF=__diff_$TT printf "$CLEANCOMPILER\t%-30s " $T -- 2.39.2