From: Enrico Tassi Date: Wed, 28 Jun 2006 08:06:34 +0000 (+0000) Subject: added gzip to log files X-Git-Tag: make_still_working~7137 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3776849e95cda45b5653419cbf173605d51731ee;p=helm.git added gzip to log files --- diff --git a/helm/software/matita/tests/TPTP/try.sh b/helm/software/matita/tests/TPTP/try.sh index e55733bff..0e494d59e 100755 --- a/helm/software/matita/tests/TPTP/try.sh +++ b/helm/software/matita/tests/TPTP/try.sh @@ -12,7 +12,7 @@ i=1 for X in $TODO; do echo -n "$X ... " LOGNAME=logs/log.`basename $X` - ../../matitac.opt $X > $LOGNAME 2>&1 + ../../matitac.opt -nodb $X | gzip -9 > $LOGNAME 2>&1 RATING=`grep "Rating" $X | sed 's/v.*//' | sed 's/(\*//'` if [ `grep "Found a proof" $LOGNAME | wc -l` -gt 0 ]; then TIME=`grep "TIME NEEDED" $LOGNAME`