Admin/isatest-makedist
changeset 14037 3b7f3eec9684
parent 14032 a6239314e380
child 14170 edd5a2ea3807
     1.1 --- a/Admin/isatest-makedist	Sun May 18 16:15:01 2003 +0200
     1.2 +++ b/Admin/isatest-makedist	Sun May 18 16:16:58 2003 +0200
     1.3 @@ -20,7 +20,8 @@
     1.4  
     1.5  LOGPREFIX=$HOME/log
     1.6  MASTERLOG=$LOGPREFIX/isatest.log
     1.7 -ERRORLOG=$HOME/var/error.log
     1.8 +ERRORDIR=$HOME/var
     1.9 +ERRORLOG=$ERRORDIR/error.log
    1.10  RUNNING=$HOME/var/running
    1.11  DISTPREFIX=$HOME/isadist
    1.12  MAKEDIST=$HOME/bin/makedist
    1.13 @@ -53,6 +54,7 @@
    1.14  
    1.15  # cleanup old error log and test-still-running files
    1.16  rm -f $ERRORLOG
    1.17 +rm -f $ERRORDIR/isatest-*.log
    1.18  rm -f $RUNNING/*.runnning
    1.19  
    1.20  export DISTPREFIX
    1.21 @@ -81,7 +83,7 @@
    1.22      echo "$HOSTNAME:$DISTLOG" >> $TMP
    1.23  
    1.24      for R in $MAILTO; do
    1.25 -	$MAIL "isabelle dist build failed" $R $TMP
    1.26 +        $MAIL "isabelle dist build failed" $R $TMP
    1.27      done
    1.28  
    1.29      rm $TMP