From: Enrico Tassi Date: Tue, 13 Dec 2005 14:14:05 +0000 (+0000) Subject: fixed_names X-Git-Tag: make_still_working~8007 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f9410c56ba4645668d5246654df1ba816ec249b1;p=helm.git fixed_names --- diff --git a/helm/matita/scripts/crontab b/helm/matita/scripts/crontab index 4221e65e9..9ab94c4d7 100644 --- a/helm/matita/scripts/crontab +++ b/helm/matita/scripts/crontab @@ -1,2 +1,3 @@ MAILTO=helm@cs.unibo.it +HOME=/home/tassi/ 10 5 * * * sh /home/tassi/helm/matita/scripts/crontab.sh diff --git a/helm/matita/scripts/crontab.sh b/helm/matita/scripts/crontab.sh index ee7c181db..648a1a709 100644 --- a/helm/matita/scripts/crontab.sh +++ b/helm/matita/scripts/crontab.sh @@ -1,12 +1,13 @@ #!/bin/bash TODAY=`date +%Y%m%d` YESTERDAY=`date -d yesterday +%Y%m%d` -TMPDIRNAME=.__${TODAY}_crontab +TMPDIRNAME=$HOME/__${TODAY}_crontab CVSROOT=":ext:$USER@marcello.cs.unibo.it:/home/faculty/PROJECTS/cvs/helm" SHELLTIME2CENTSPHP=helm/matita/scripts/shell_time2cents.php SHELLADDERPHP=helm/matita/scripts/shell_adder.php COMMONPHP=helm/matita/scripts/public_html/common.php + OLD=$PWD rm -rf $TMPDIRNAME mkdir $TMPDIRNAME @@ -71,5 +72,5 @@ EOT fi cd $OLD -rm -rf $TMPDIRNAME +#rm -rf $TMPDIRNAME diff --git a/helm/matita/scripts/profile_cvs.sh b/helm/matita/scripts/profile_cvs.sh index a0fb848a9..ea4e43dfa 100755 --- a/helm/matita/scripts/profile_cvs.sh +++ b/helm/matita/scripts/profile_cvs.sh @@ -1,6 +1,6 @@ #!/bin/bash MARK=`date +%Y%m%d%H%M` -TMPDIRNAME=.__$MARK +TMPDIRNAME=__${MARK}_compilation CVSROOT=":ext:$USER@marcello.cs.unibo.it:/home/faculty/PROJECTS/cvs/helm" function testit {