src/Pure/mk

 # Author: Markus Wenzel, TU Muenchen
 # License: GPL (GNU GENERAL PUBLIC LICENSE)
 #
 # mk - build Pure Isabelle.
 #
-# Assumes to be called via Isabelle make utility (cf. IsaMakefile).
+# Requires proper Isabelle settings environment (cf. IsaMakefile).
 
 
 ## diagnostics
 
 function usage()

   echo
   echo "Usage: $PRG [OPTIONS]"
   echo
   echo "  Make Pure Isabelle."
   echo
-  echo "    -r           just prepare RAW image"
+  echo "    -C           tell ML system to copy output image"
+  echo "    -r           prepare RAW image only"
   echo
   exit 1
 }
 
 function fail()

 
 ## process command line
 
 # options
 
+COPY=""
 RAW=""
 
-while getopts "r" OPT
+while getopts "Cr" OPT
 do
   case "$OPT" in
+    C)
+      COPY="-C"
+      ;;
     r)
       RAW=true
       ;;
     \?)
       usage

 if [ -z "$RAW" ]; then
   ITEM="Pure"
   echo "Building $ITEM ..."
   LOG="$LOGDIR/$ITEM"
 
-  "$ISABELLE" \
+  "$ISABELLE" $COPY \
     -e "val ml_system = \"$ML_SYSTEM\";" \
     -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \
     -c -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1
   RC="$?"
 else
   ITEM="RAW"
   echo "Building $ITEM ..."
   LOG="$LOGDIR/$ITEM"
 
-  "$ISABELLE" \
+  "$ISABELLE" $COPY \
     -e "val ml_system = \"$ML_SYSTEM\";" \
     -e "use\"$COMPAT\" handle _ => exit 1;;" \
     -q -w RAW_ML_SYSTEM RAW > "$LOG" 2>&1
   RC="$?"
 fi