# HG changeset patch # User wenzelm # Date 967642219 -7200 # Node ID 07f2487f1abbabd6ceafbca41ff575f75f970475 # Parent 9ca034ef256c9bca8ed60091a3a898fabef23d79 tuned; diff -r 9ca034ef256c -r 07f2487f1abb etc/settings --- a/etc/settings Wed Aug 30 15:27:53 2000 +0200 +++ b/etc/settings Wed Aug 30 15:30:19 2000 +0200 @@ -19,8 +19,8 @@ "$ISABELLE_HOME/contrib/polyml" \ "$ISABELLE_HOME/../polyml") ML_PLATFORM=$($POLYML_HOME/bin/polyml-platform 2>/dev/null) +ML_SYSTEM=$($POLYML_HOME/bin/polyml-version 2>/dev/null) ML_HOME=$POLYML_HOME/$ML_PLATFORM -ML_SYSTEM=$($POLYML_HOME/bin/polyml-version 2>/dev/null) ML_OPTIONS="-h 30000" # Standard ML of New Jersey 110 or later