diff -r 5de31ddf9c03 -r 7268a5f425f8 src/Pure/mk
--- a/src/Pure/mk	Tue Jan 16 00:22:43 2001 +0100
+++ b/src/Pure/mk	Tue Jan 16 00:23:14 2001 +0100
@@ -93,7 +93,7 @@
   "$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
+    -f -c -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1
   RC="$?"
 else
   ITEM="RAW"
@@ -102,7 +102,7 @@
 
   "$ISABELLE" $COPY \
     -e "val ml_system = \"$ML_SYSTEM\";" \
-    -e "use\"$COMPAT\" handle _ => exit 1;;" \
+    -e "use\"$COMPAT\" handle _ => exit 1;" \
     -q -w RAW_ML_SYSTEM RAW > "$LOG" 2>&1
   RC="$?"
 fi