# HG changeset patch
# User kleing
# Date 1051276656 -7200
# Node ID 09f6f2fefb255e3a516f40775bcc541fe9a90333
# Parent  019342d03d81b3c68653bee7d893996b87a80653
no need to be nice everywhere

diff -r 019342d03d81 -r 09f6f2fefb25 Admin/isatest-makeall
--- a/Admin/isatest-makeall	Fri Apr 25 11:18:41 2003 +0200
+++ b/Admin/isatest-makeall	Fri Apr 25 15:17:36 2003 +0200
@@ -51,10 +51,13 @@
 
 [ -d $DISTPREFIX ] || fail "$DISTPREFIX is not a directory."
 
+NICE=nice
+
 case $HOSTNAME in
         atbroy51)
 	MFLAGS="-j 2"
 	# MFLAGS=""
+  NICE=""
 	;;
 
         atbroy31)
@@ -98,7 +101,7 @@
     echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1
 
     cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings
-    nice $DISTPREFIX/Isabelle/bin/isatool makeall $MFLAGS all >> $TESTLOG 2>&1 
+    $NICE $DISTPREFIX/Isabelle/bin/isatool makeall $MFLAGS all >> $TESTLOG 2>&1 
 
     if [ $? -eq 0 ]
     then