# HG changeset patch
# User wenzelm
# Date 1323861044 -3600
# Node ID 4bb0fc92247b014e3675e3a5da9084236c0c3f96
# Parent  93eda35a83779c348a0747169e0fd95c84795c51
some full isatest runs, which include benchmark targets;

diff -r 93eda35a8377 -r 4bb0fc92247b Admin/isatest/isatest-makeall
--- a/Admin/isatest/isatest-makeall	Wed Dec 14 12:02:02 2011 +0100
+++ b/Admin/isatest/isatest-makeall	Wed Dec 14 12:10:44 2011 +0100
@@ -46,6 +46,8 @@
 
 [ -d $DISTPREFIX ] || fail "$DISTPREFIX is not a directory."
 
+TARGETS=all
+
 # make file flags and nice setup for different target platforms
 case $HOSTNAME in
     atbroy51)
@@ -69,6 +71,7 @@
   
     macbroy2)
         MFLAGS="-k"
+        TARGETS=full
         NICE=""
         ;;
 
@@ -97,6 +100,12 @@
         NICE=""
         ;;
 
+    macbroy30)
+        MFLAGS="-k"
+        TARGETS=full
+        NICE=""
+        ;;
+
     *)
         MFLAGS="-k"
         # be nice by default
@@ -119,7 +128,7 @@
   TOOL="$ISABELLE_TOOL make $MFLAGS $TARGETS"
 else
   DIR="."
-  TOOL="$ISABELLE_TOOL makeall $MFLAGS all"
+  TOOL="$ISABELLE_TOOL makeall $MFLAGS $TARGETS"
 fi
 
 IDENT=$(cat "$DISTPREFIX/ISABELLE_IDENT")