author | wenzelm |
Wed, 30 Aug 2000 15:30:19 +0200 | |
changeset 9745 | 07f2487f1abb |
parent 9744 | 9ca034ef256c |
child 9746 | 64b803edef39 |
etc/settings | file | annotate | diff | comparison | revisions |
--- 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