equal
deleted
inserted
replaced
15 #ML_SYSTEM=polyml-2.07 |
15 #ML_SYSTEM=polyml-2.07 |
16 #ML_HOME=/usr/local/ldist/DIR/polyml/polyml/solaris2 |
16 #ML_HOME=/usr/local/ldist/DIR/polyml/polyml/solaris2 |
17 #ML_OPTIONS="-h 30000" |
17 #ML_OPTIONS="-h 30000" |
18 |
18 |
19 # Poly/ML 3.1 |
19 # Poly/ML 3.1 |
20 #ML_SYSTEM=polyml-3.1 |
20 ML_SYSTEM=polyml-3.1 |
21 #ML_HOME=/usr/local/ldist/DIR/polyml-3.1/polyml/sunos5.4 |
21 ML_HOME=/usr/local/ldist/DIR/polyml-3.1/polyml/sunos5.4 |
22 #ML_OPTIONS="-h 30000" |
22 ML_OPTIONS="-h 30000" |
23 #LM_LICENSE_FILE=$ML_HOME/license.dat |
23 LM_LICENSE_FILE=$ML_HOME/license.dat |
24 |
24 |
25 # Standard ML of New Jersey 0.93 |
25 # Standard ML of New Jersey 0.93 |
26 #ML_SYSTEM=smlnj-0.93 |
26 #ML_SYSTEM=smlnj-0.93 |
27 #ML_HOME=/usr/local/ldist/DIR/sml-0.93/src |
27 #ML_HOME=/usr/local/ldist/DIR/sml-0.93/src |
28 #ML_OPTIONS="" |
28 #ML_OPTIONS="" |
31 #ML_SYSTEM=smlnj-109 |
31 #ML_SYSTEM=smlnj-109 |
32 #ML_HOME=/usr/proj/smlnj/109.32/bin |
32 #ML_HOME=/usr/proj/smlnj/109.32/bin |
33 #ML_OPTIONS="@SMLdebug=/dev/null" |
33 #ML_OPTIONS="@SMLdebug=/dev/null" |
34 |
34 |
35 # Standard ML of New Jersey 110 or later |
35 # Standard ML of New Jersey 110 or later |
36 ML_SYSTEM=smlnj-110 |
36 #ML_SYSTEM=smlnj-110 |
37 ML_HOME=/usr/local/smlnj-110/bin |
37 #ML_HOME=/usr/local/smlnj-110/bin |
38 ML_OPTIONS="@SMLdebug=/dev/null" |
38 #ML_OPTIONS="@SMLdebug=/dev/null" |
39 |
39 |
40 # MLWorks 1.0r2 or later -- still EXPERIMENTAL!! |
40 # MLWorks 1.0r2 or later -- still EXPERIMENTAL!! |
41 #ML_SYSTEM=mlworks |
41 #ML_SYSTEM=mlworks |
42 #ML_HOME=/usr/local/mlworks/bin |
42 #ML_HOME=/usr/local/mlworks/bin |
43 #ML_OPTIONS="" |
43 #ML_OPTIONS="" |