# HG changeset patch # User wenzelm # Date 952340679 -3600 # Node ID e708af969264707de8d430dd4aacd8edc8f01305 # Parent 4417e588d9f7d928e06a0f464a5060794ff6fa47 new Poly/ML setup made default; diff -r 4417e588d9f7 -r e708af969264 etc/settings --- a/etc/settings Sat Mar 04 13:28:21 2000 +0100 +++ b/etc/settings Mon Mar 06 12:04:39 2000 +0100 @@ -11,11 +11,18 @@ ## Uncomment and adapt one of the sections below. Note that ML_HOME ## specifies the location of the actual compiler binaries. +# Poly/ML 3.x +POLYML_HOME=$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_OPTIONS="-h 30000" + # Standard ML of New Jersey 110 or later -ML_SYSTEM=smlnj-110 -ML_HOME=$ISABELLE_HOME/../smlnj/bin -ML_OPTIONS="@SMLdebug=/dev/null" -ML_PLATFORM=$(eval $($ML_HOME/.arch-n-opsys 2>/dev/null); echo $HEAP_SUFFIX) +#ML_SYSTEM=smlnj-110 +#ML_HOME=$ISABELLE_HOME/../smlnj/bin +#ML_OPTIONS="@SMLdebug=/dev/null" +#ML_PLATFORM=$(eval $($ML_HOME/.arch-n-opsys 2>/dev/null); echo $HEAP_SUFFIX) # MLWorks 2.0 or later #ML_SYSTEM=mlworks @@ -29,13 +36,6 @@ #ML_OPTIONS="-h 30000" #ML_PLATFORM="" -# Poly/ML 3.1 -#ML_SYSTEM=polyml-3.1 -#ML_HOME=/usr/local/ldist/DIR/polyml-3.1/polyml/sunos5.4 -#ML_OPTIONS="-h 30000" -#ML_PLATFORM="" -#LM_LICENSE_FILE=$ML_HOME/license.dat - # Standard ML of New Jersey 0.93 #ML_SYSTEM=smlnj-0.93 #ML_HOME=/usr/local/ldist/DIR/sml-0.93/src