# HG changeset patch
# User wenzelm
# Date 940416776 -7200
# Node ID 56e91ac0f07489a115ec401da239993d1e74c932
# Parent  6e9669c311ae85ea800a619c54ad1c617b7a37a5
option -m TARGET;

diff -r 6e9669c311ae -r 56e91ac0f074 build
--- a/build	Wed Oct 20 11:06:47 1999 +0200
+++ b/build	Wed Oct 20 12:52:56 1999 +0200
@@ -14,6 +14,7 @@
 
 PRG=$(basename $0)
 
+export THIS_IS_ISABELLE_BUILD=true
 ISABELLE_HOME=$(dirname $0)
 . $ISABELLE_HOME/lib/scripts/getsettings || \
   { echo "$PRG probably not called from its original place!"; exit 2; }
@@ -30,6 +31,7 @@
   echo "    -a           all logics"
   echo "    -b           batch mode"
   echo "    -i           make images"
+  echo "    -m TARGET    make this target"
   echo "    -t           make test"
   echo
   echo "  Compile the named LOGICS (default $ISABELLE_LOGIC), or all object logics"
@@ -51,10 +53,9 @@
 
 ALL=""
 BATCH=""
-IMAGES=""
-TEST=""
+TARGETS=""
 
-while getopts "abit" OPT
+while getopts "abim:t" OPT
 do
   case "$OPT" in
     a)
@@ -64,10 +65,13 @@
       BATCH=true
       ;;
     i)
-      IMAGES=images
+      TARGETS="$TARGETS images"
+      ;;
+    m)
+      TARGETS="$TARGETS $OPTARG"
       ;;
     t)
-      TEST=test
+      TARGETS="$TARGETS test"
       ;;
     \?)
       usage
@@ -160,12 +164,9 @@
 HOST=$(hostname)
 echo "Started at $DATE ($HOST)"
 
-unset ISABELLE_SETTINGS_PRESENT
-export THIS_IS_ISABELLE_BUILD=true
-
 for L in $MAKE_LOGICS
 do
-  ( cd $ISABELLE_HOME/src/$L; $ISATOOL make $IMAGES $TEST )
+  ( cd $ISABELLE_HOME/src/$L; $ISATOOL make $TARGETS )
 done
 
 echo -n "Finished at "; date