--- a/src/Pure/mk Sat Jun 11 23:18:06 2005 +0200
+++ b/src/Pure/mk Sat Jun 11 23:19:36 2005 +0200
@@ -90,6 +90,7 @@
"$ISABELLE" $COPY \
-e "val ml_system = \"$ML_SYSTEM\";" \
+ -e "val ml_platform = \"$ML_PLATFORM\";" \
-e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \
-f -c -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1
RC="$?"
@@ -100,6 +101,7 @@
"$ISABELLE" $COPY \
-e "val ml_system = \"$ML_SYSTEM\";" \
+ -e "val ml_platform = \"$ML_PLATFORM\";" \
-e "use\"$COMPAT\" handle _ => exit 1;" \
-q -w RAW_ML_SYSTEM RAW > "$LOG" 2>&1
RC="$?"