# HG changeset patch
# User wenzelm
# Date 970144562 -7200
# Node ID 3c21a2e616e7ea0a9b152752d54782a5f7092500
# Parent  746263fbcbfdc825d0a381a6799a072222b54044
support copy option;

diff -r 746263fbcbfd -r 3c21a2e616e7 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Thu Sep 28 14:35:42 2000 +0200
+++ b/src/Pure/IsaMakefile	Thu Sep 28 14:36:02 2000 +0200
@@ -51,11 +51,17 @@
 	@./mk
 
 
-## RAW
+## special targets
+
+Pure-copied:
+	@./mk -C
 
 RAW:
 	@./mk -r
 
+RAW-copied:
+	@./mk -Cr
+
 
 ## clean
 
diff -r 746263fbcbfd -r 3c21a2e616e7 src/Pure/mk
--- a/src/Pure/mk	Thu Sep 28 14:35:42 2000 +0200
+++ b/src/Pure/mk	Thu Sep 28 14:36:02 2000 +0200
@@ -6,7 +6,7 @@
 #
 # mk - build Pure Isabelle.
 #
-# Assumes to be called via Isabelle make utility (cf. IsaMakefile).
+# Requires proper Isabelle settings environment (cf. IsaMakefile).
 
 
 ## diagnostics
@@ -18,7 +18,8 @@
   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
 }
@@ -34,11 +35,15 @@
 
 # options
 
+COPY=""
 RAW=""
 
-while getopts "r" OPT
+while getopts "Cr" OPT
 do
   case "$OPT" in
+    C)
+      COPY="-C"
+      ;;
     r)
       RAW=true
       ;;
@@ -85,7 +90,7 @@
   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
@@ -95,7 +100,7 @@
   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