# HG changeset patch # User wenzelm # Date 967642073 -7200 # Node ID 9ca034ef256c9bca8ed60091a3a898fabef23d79 # Parent d18d5c4a1f809532c037c6ef9bf987ec2230a0e3 use polyml-version; diff -r d18d5c4a1f80 -r 9ca034ef256c etc/settings --- a/etc/settings Wed Aug 30 14:45:50 2000 +0200 +++ b/etc/settings Wed Aug 30 15:27:53 2000 +0200 @@ -14,13 +14,13 @@ # binaries. Do not invent new ML system names unless you know what # you are doing. -# Poly/ML 3.x +# Poly/ML 3.x or later POLYML_HOME=$(choosefrom \ "$ISABELLE_HOME/contrib/polyml" \ "$ISABELLE_HOME/../polyml") ML_PLATFORM=$($POLYML_HOME/bin/polyml-platform 2>/dev/null) ML_HOME=$POLYML_HOME/$ML_PLATFORM -ML_SYSTEM=polyml-3.x +ML_SYSTEM=$($POLYML_HOME/bin/polyml-version 2>/dev/null) ML_OPTIONS="-h 30000" # Standard ML of New Jersey 110 or later