# HG changeset patch
# User isatest
# Date 1046437914 -3600
# Node ID fe83f22317678368dd1b12423835bafefb23c59e
# Parent  8dd150d36c6536e9ab208a160b263e314efb459e
case distinction on host for makefile flags

diff -r 8dd150d36c65 -r fe83f2231767 Admin/isatest-makeall
--- a/Admin/isatest-makeall	Thu Feb 27 18:22:49 2003 +0100
+++ b/Admin/isatest-makeall	Fri Feb 28 14:11:54 2003 +0100
@@ -8,7 +8,7 @@
 #              Send email if it fails.
 
 ## global settings
-MAILTO="kleing@in.tum.de nipkow@in.tum.de wenzelm@in.tum.de berghofe@in.tum.de schirmer@in.tum.de lp15@cam.ac.uk"
+MAILTO="kleing@in.tum.de nipkow@in.tum.de berghofe@in.tum.de schirmer@in.tum.de lp15@cam.ac.uk"
 
 LOGPREFIX=~/log
 
@@ -51,6 +51,31 @@
 
 [ -d $DISTPREFIX ] || fail "$DISTPREFIX is not a directory."
 
+case $HOSTNAME in
+        atbroy51)
+	MFLAGS="-j 2"
+	# MFLAGS=""
+	;;
+
+        atbroy31)
+        MFLAGS="-j 5"
+        ;;
+	
+	atbroy12)
+	MFLAGS="-j 5"
+	;;
+
+	sunbroy2)
+	MFLAGS="-j 4"
+	;;
+
+   	*)
+	MFLAGS=""
+        ;;
+esac
+
+
+
 LOGS=""
 
 for SETTINGS in $@; do
@@ -69,7 +94,7 @@
     echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1
 
     cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings
-    nice $DISTPREFIX/Isabelle/bin/isatool makeall -j 2 all >> $TESTLOG 2>&1 
+    nice $DISTPREFIX/Isabelle/bin/isatool makeall $MFLAGS all >> $TESTLOG 2>&1 
 
     if [ $? -eq 0 ]
     then