# HG changeset patch
# User isatest
# Date 1191163906 -7200
# Node ID fd6d2040f89b5465ec1ae390599896da26b3d7b1
# Parent  47bb1e380d83830531d52506eb455570c70c71e5
fix shell quoting confusion

diff -r 47bb1e380d83 -r fd6d2040f89b Admin/isatest/isatest-makeall
--- a/Admin/isatest/isatest-makeall	Sun Sep 30 16:20:42 2007 +0200
+++ b/Admin/isatest/isatest-makeall	Sun Sep 30 16:51:46 2007 +0200
@@ -97,9 +97,11 @@
   TARGETS="$2"
   shift 2
   ISABELLE_HOME="$($ISATOOL getenv -b ISABELLE_HOME)"
-  TOOL="cd $ISABELLE_HOME/$LOGIC; $NICE $ISATOOL make $MFLAGS $TARGETS"
+  DIR="$ISABELLE_HOME/$LOGIC"
+  TOOL="$ISATOOL make $MFLAGS $TARGETS"
 else
-  TOOL="$NICE $ISATOOL makeall $MFLAGS all"
+  DIR="."
+  TOOL="$ISATOOL makeall $MFLAGS all"
 fi
 
 # main test loop
@@ -121,7 +123,7 @@
     echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1
 
     cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings
-    (ulimit -t $MAXTIME; $TOOL >> $TESTLOG 2>&1)
+    (ulimit -t $MAXTIME; cd $DIR; $NICE $TOOL >> $TESTLOG 2>&1)
 
     if [ $? -eq 0 ]
     then
diff -r 47bb1e380d83 -r fd6d2040f89b Admin/isatest/isatest-settings
--- a/Admin/isatest/isatest-settings	Sun Sep 30 16:20:42 2007 +0200
+++ b/Admin/isatest/isatest-settings	Sun Sep 30 16:51:46 2007 +0200
@@ -11,7 +11,7 @@
 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 krauss@in.tum.de"
+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"
 
 LOGPREFIX=$HOME/log
 MASTERLOG=$LOGPREFIX/isatest.log