use global settings for isatest-doc
authorkleing
Thu Jun 30 05:27:40 2005 +0200 (2005-06-30 ago)
changeset 16615e665dafdd2b8
parent 16614 a493a50e6c0a
child 16616 491d8dbdb3b8
use global settings for isatest-doc
Admin/isatest-doc
Admin/isatest-settings
     1.1 --- a/Admin/isatest-doc	Wed Jun 29 15:13:44 2005 +0200
     1.2 +++ b/Admin/isatest-doc	Thu Jun 30 05:27:40 2005 +0200
     1.3 @@ -10,28 +10,23 @@
     1.4  
     1.5  . ~/.bashrc
     1.6  
     1.7 -## settings
     1.8 -MAILTO="kleing@cse.unsw.edu.au nipkow@in.tum.de haftmann@in.tum.de berghofe@in.tum.de lp15@cam.ac.uk makarius@sketis.net"
     1.9 +## global settings
    1.10 +. ~/admin/isatest-settings
    1.11  
    1.12  DOCDIR=$HOME/Doc
    1.13 -DISTPREFIX=~/tmp/isadist
    1.14  
    1.15  MAXTIME=1800
    1.16  
    1.17  ISABELLE_DEVEL=$DISTPREFIX/Isabelle
    1.18  DATE=$(date "+%Y-%m-%d")
    1.19  
    1.20 -LOG=~/log/isatest-doc-$DATE.log
    1.21 -MASTERLOG=~/log/isatest.log
    1.22 +LOG=$LOGPREFIX/isatest-doc-$DATE.log
    1.23  
    1.24  SHORT=sun-poly
    1.25  SETTINGS=~/settings/$SHORT
    1.26  
    1.27  ISATOOL=$ISABELLE_DEVEL/bin/isatool
    1.28      
    1.29 -ERRORDIR=$HOME/var
    1.30 -ERRORLOG=$ERRORDIR/error.log
    1.31 -RUNNING=$HOME/var/running
    1.32  
    1.33  MAIL=~/afp/release/admin/mail-attach
    1.34  
     2.1 --- a/Admin/isatest-settings	Wed Jun 29 15:13:44 2005 +0200
     2.2 +++ b/Admin/isatest-settings	Thu Jun 30 05:27:40 2005 +0200
     2.3 @@ -1,3 +1,4 @@
     2.4 +# -*- shell-script -*-
     2.5  # $Id$
     2.6  # Author: Gerwin Klein, NICTA
     2.7  #