Admin/isatest/isatest-settings
author kleing
Sat Oct 11 03:54:34 2008 +0200 (2008-10-11)
changeset 28567 3caee0cd91d8
parent 28539 bdb308737bfd
child 29926 7dac794eec91
permissions -rw-r--r--
change DISTPREFIX to not use yet another filesystem
     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=/home/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 makarius@sketis.net haftmann@in.tum.de krauss@in.tum.de"
    15 
    16 LOGPREFIX=$HOME/log
    17 MASTERLOG=$LOGPREFIX/isatest.log
    18 LOGSERVER=macbroy23.informatik.tu-muenchen.de
    19 
    20 ERRORDIR=$HOME/var
    21 ERRORLOG=$ERRORDIR/error.log
    22 
    23 RUNNING=$HOME/var/running
    24 
    25 DISTPREFIX=$HOME/isadist
    26 
    27 # this function avoids NFS inconsistencies with multiple writers by
    28 # sshing to one central machine and writing locally. There is stil a
    29 # race condition, but at least it should not corrupt a whole set of entries
    30 # any more.
    31 function log()
    32 {
    33   MSG="$1"
    34   TIMESTAMP="$(date)"
    35   echo "[$TIMESTAMP $HOSTNAME $PRG]: $MSG" | ssh $LOGSERVER "cat >> $MASTERLOG"
    36 }