Admin/isatest/isatest-settings
changeset 22410 da313b67a04d
child 23070 c5b896d9788c
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/Admin/isatest/isatest-settings	Mon Mar 05 22:12:20 2007 +0100
     1.3 @@ -0,0 +1,24 @@
     1.4 +# -*- shell-script -*-
     1.5 +# $Id$
     1.6 +# Author: Gerwin Klein, NICTA
     1.7 +#
     1.8 +# DESCRIPTION: common settings for the isatest-* scripts
     1.9 +
    1.10 +# source bashrc, we're called by cron
    1.11 +. ~/.bashrc
    1.12 +
    1.13 +# canoncical home for all platforms
    1.14 +HOME=/home/isatest
    1.15 +
    1.16 +## send email on failure to
    1.17 +MAILTO="kleing@cse.unsw.edu.au nipkow@in.tum.de berghofe@in.tum.de schirmer@in.tum.de lp15@cam.ac.uk makarius@sketis.net haftmann@in.tum.de"
    1.18 +
    1.19 +LOGPREFIX=$HOME/log
    1.20 +MASTERLOG=$LOGPREFIX/isatest.log
    1.21 +
    1.22 +ERRORDIR=$HOME/var
    1.23 +ERRORLOG=$ERRORDIR/error.log
    1.24 +
    1.25 +RUNNING=$HOME/var/running
    1.26 +
    1.27 +DISTPREFIX=$HOME/tmp/isadist