diff -r 5f7c9c82b05e -r da313b67a04d Admin/isatest-settings
--- a/Admin/isatest-settings	Mon Mar 05 10:14:32 2007 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,24 +0,0 @@
-# -*- 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