use global settings for isatest-doc
authorkleing
Thu, 30 Jun 2005 05:27:40 +0200
changeset 16615 e665dafdd2b8
parent 16614 a493a50e6c0a
child 16616 491d8dbdb3b8
use global settings for isatest-doc
Admin/isatest-doc
Admin/isatest-settings
--- a/Admin/isatest-doc	Wed Jun 29 15:13:44 2005 +0200
+++ b/Admin/isatest-doc	Thu Jun 30 05:27:40 2005 +0200
@@ -10,28 +10,23 @@
 
 . ~/.bashrc
 
-## settings
-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"
+## global settings
+. ~/admin/isatest-settings
 
 DOCDIR=$HOME/Doc
-DISTPREFIX=~/tmp/isadist
 
 MAXTIME=1800
 
 ISABELLE_DEVEL=$DISTPREFIX/Isabelle
 DATE=$(date "+%Y-%m-%d")
 
-LOG=~/log/isatest-doc-$DATE.log
-MASTERLOG=~/log/isatest.log
+LOG=$LOGPREFIX/isatest-doc-$DATE.log
 
 SHORT=sun-poly
 SETTINGS=~/settings/$SHORT
 
 ISATOOL=$ISABELLE_DEVEL/bin/isatool
     
-ERRORDIR=$HOME/var
-ERRORLOG=$ERRORDIR/error.log
-RUNNING=$HOME/var/running
 
 MAIL=~/afp/release/admin/mail-attach
 
--- a/Admin/isatest-settings	Wed Jun 29 15:13:44 2005 +0200
+++ b/Admin/isatest-settings	Thu Jun 30 05:27:40 2005 +0200
@@ -1,3 +1,4 @@
+# -*- shell-script -*-
 # $Id$
 # Author: Gerwin Klein, NICTA
 #