diff -r 8aec6154bb17 -r 88e34d7af6e3 Admin/isatest/isatest-makeall
--- a/Admin/isatest/isatest-makeall	Sat Sep 29 08:58:57 2007 +0200
+++ b/Admin/isatest/isatest-makeall	Sat Sep 29 10:04:52 2007 +0200
@@ -18,11 +18,14 @@
 function usage()
 {
   echo
-  echo "Usage: $PRG settings1 [settings2 ...]"
+  echo "Usage: $PRG [-l logic targets] settings1 [settings2 ...]"
   echo
   echo "  Runs isatool makeall for specified settings."
   echo "  Leaves messages in ${ERRORLOG} and ${LOGPREFIX} if it fails."
   echo
+  echo "Examples:"
+  echo "  $PRG ~/settings/at-poly ~/settings/at-sml"
+  echo "  $PRG -l HOL \"HOL-Library HOL-Bali\" ~/settings/at-poly"
   exit 1
 }
 
@@ -83,6 +86,22 @@
         ;;
 esac
 
+ISATOOL="$DISTPREFIX/Isabelle/bin/isatool"
+
+[ -x $ISATOOL ] || fail "Cannot run $ISATOOL"
+
+if [ "$1" = "-l" ]; then
+  shift
+  [ "$#" -lt "3" ] && usage
+  LOGIC="$1"
+  TARGETS="$2"
+  shift 2
+  ISABELLE_HOME="$($ISATOOL getenv -b ISABELLE_HOME)"
+  TOOL="cd $ISABELLE_HOME/$LOGIC; $NICE $ISATOOL make $MFLAGS $TARGETS"
+else
+  TOOL="$NICE $ISATOOL makeall $MFLAGS all"
+fi
+
 # main test loop
 
 for SETTINGS in $@; do
@@ -102,7 +121,7 @@
     echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1
 
     cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings
-    (ulimit -t $MAXTIME; $NICE $DISTPREFIX/Isabelle/bin/isatool makeall $MFLAGS all >> $TESTLOG 2>&1)
+    (ulimit -t $MAXTIME; $TOOL >> $TESTLOG 2>&1)
 
     if [ $? -eq 0 ]
     then