added a getter maps updater

[helm.git] / helm / matita / scripts / do_tests.sh

diff --git a/helm/matita/scripts/do_tests.sh b/helm/matita/scripts/do_tests.sh
index b95ca578cdbababbe0bfd9908e42f962c446b7c9..737ea7c5efd42de28d6359f0126f56ba96ee5068 100755 (executable)
--- a/helm/matita/scripts/do_tests.sh
+++ b/helm/matita/scripts/do_tests.sh
@@ -29,7 +29,7 @@ TMP=.__temp.txt
 
 for T in $TODO; do
   echo -en "$COMPILER\t$T\t"
-  /usr/bin/time -o $TMP -f "%E\t%U\t%S" $COMPILER $T >> $LOGFILE 2>&1
+  /usr/bin/time --quiet -o $TMP -f "%E\t%U\t%S" $COMPILER $T >> $LOGFILE 2>&1
   if [ $? = 0 ]; then
     echo -e "$OK\t`cat $TMP`\t$DO_TESTS_EXTRA"
   else