# 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