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")