# HG changeset patch
# User wenzelm
# Date 1159479775 -7200
# Node ID cc436bcdd5fccea5b9732d3617210196344b4a57
# Parent  69f83b886422d58171fe8db6b8da6a9858566adf
added share_data (dummy);

diff -r 69f83b886422 -r cc436bcdd5fc src/Pure/mk
--- a/src/Pure/mk	Thu Sep 28 23:42:53 2006 +0200
+++ b/src/Pure/mk	Thu Sep 28 23:42:55 2006 +0200
@@ -91,6 +91,7 @@
   "$ISABELLE" $COPY \
     -e "val ml_system = \"$ML_SYSTEM\";" \
     -e "val ml_platform = \"$ML_PLATFORM\";" \
+    -e "val share_data = NONE: ('a -> 'a) option;" \
     -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \
     -f -c -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1
   RC="$?"