diff -r 5f7c9c82b05e -r da313b67a04d Admin/isatest/isatest-settings
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/isatest/isatest-settings	Mon Mar 05 22:12:20 2007 +0100
@@ -0,0 +1,24 @@
+# -*- shell-script -*-
+# $Id$
+# Author: Gerwin Klein, NICTA
+#
+# DESCRIPTION: common settings for the isatest-* scripts
+
+# source bashrc, we're called by cron
+. ~/.bashrc
+
+# canoncical home for all platforms
+HOME=/home/isatest
+
+## send email on failure to
+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"
+
+LOGPREFIX=$HOME/log
+MASTERLOG=$LOGPREFIX/isatest.log
+
+ERRORDIR=$HOME/var
+ERRORLOG=$ERRORDIR/error.log
+
+RUNNING=$HOME/var/running
+
+DISTPREFIX=$HOME/tmp/isadist