fix

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

diff --git a/helm/matita/scripts/crontab.sh b/helm/matita/scripts/crontab.sh
index d8ac761b3e01427dbb89fe3e3334058b6ae78a04..03ce5ce9541c5f3d3a3ad8ac63b88e97467345cf 100644 (file)
--- a/helm/matita/scripts/crontab.sh
+++ b/helm/matita/scripts/crontab.sh
@@ -7,10 +7,10 @@ rm -rf $TMPDIRNAME
 mkdir $TMPDIRNAME
 cd $TMPDIRNAME
 cvs -d $CVSROOT co helm/matita/scripts 1>/dev/null 2>/dev/null
-bash helm/matita/scripts/profile_cvs.sh > LOG 1>&2
+helm/matita/scripts/profile_cvs.sh 2> LOG
 
 cat <<EOT
-WEB INTERFACE
+REPORT FOR `date`
 http://mowgli.cs.unibo.it/tassi/bench.php
 
 DAILY BENCHMARK REPORT