Admin/isatest-settings
author wenzelm
Tue Jul 05 16:49:15 2005 +0200 (2005-07-05)
changeset 16693 75f39d66425d
parent 16616 491d8dbdb3b8
child 17446 f869b73b71ec
permissions -rw-r--r--
fixed regexp grouping;
     1 # -*- shell-script -*-
     2 # $Id$
     3 # Author: Gerwin Klein, NICTA
     4 #
     5 # DESCRIPTION: common settings for the isatest-* scripts
     6 
     7 # source bashrc, we're called by cron
     8 . ~/.bashrc
     9 
    10 # canoncical home for all platforms
    11 HOME=/usr/stud/isatest
    12 
    13 ## send email on failure to
    14 MAILTO="kleing@cse.unsw.edu.au nipkow@in.tum.de berghofe@in.tum.de schirmer@in.tum.de lp15@cam.ac.uk skalberg@in.tum.de makarius@sketis.net haftmann@in.tum.de"
    15 
    16 LOGPREFIX=$HOME/log
    17 MASTERLOG=$LOGPREFIX/isatest.log
    18 
    19 ERRORDIR=$HOME/var
    20 ERRORLOG=$ERRORDIR/error.log
    21 
    22 RUNNING=$HOME/var/running
    23 
    24 DISTPREFIX=$HOME/tmp/isadist