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