author | wenzelm |
Thu, 28 Sep 2006 23:42:55 +0200 | |
changeset 20776 | cc436bcdd5fc |
parent 20775 | 69f83b886422 |
child 20777 | 00e560b6c112 |
src/Pure/mk | file | annotate | diff | comparison | revisions |
--- 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="$?"