# HG changeset patch
# User wenzelm
# Date 1118524776 -7200
# Node ID 65e2df6d8e102f70529c612280c46189777aefac
# Parent  de1ab9e8ed4f78441e2b98be8c634aaed5687b53
pass ml_platform;

diff -r de1ab9e8ed4f -r 65e2df6d8e10 src/Pure/mk
--- 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="$?"