changeset 9745 | 07f2487f1abb |
parent 9744 | 9ca034ef256c |
child 9759 | 8e835ebc862f |
--- 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