equal
deleted
inserted
replaced
10 |
10 |
11 ## Uncomment and adapt one of the sections below. Note that ML_HOME |
11 ## Uncomment and adapt one of the sections below. Note that ML_HOME |
12 ## specifies the location of the actual compiler binaries. |
12 ## specifies the location of the actual compiler binaries. |
13 |
13 |
14 # Standard ML of New Jersey 110 or later |
14 # Standard ML of New Jersey 110 or later |
15 ML_SYSTEM=smlnj-110 |
15 #ML_SYSTEM=smlnj-110 |
16 ML_HOME=/usr/local/smlnj-110/bin |
16 #ML_HOME=/usr/local/smlnj-110/bin |
17 ML_OPTIONS="@SMLdebug=/dev/null" |
17 #ML_OPTIONS="@SMLdebug=/dev/null" |
18 |
18 |
19 # MLWorks 2.0 or later |
19 # MLWorks 2.0 or later |
20 #ML_SYSTEM=mlworks |
20 #ML_SYSTEM=mlworks |
21 #ML_HOME=/usr/local/mlworks/bin |
21 #ML_HOME=/usr/local/mlworks/bin |
22 #ML_OPTIONS="" |
22 #ML_OPTIONS="" |
25 #ML_SYSTEM=polyml-2.07 |
25 #ML_SYSTEM=polyml-2.07 |
26 #ML_HOME=/usr/local/ldist/DIR/polyml/polyml/solaris2 |
26 #ML_HOME=/usr/local/ldist/DIR/polyml/polyml/solaris2 |
27 #ML_OPTIONS="-h 30000" |
27 #ML_OPTIONS="-h 30000" |
28 |
28 |
29 # Poly/ML 3.1 |
29 # Poly/ML 3.1 |
30 #ML_SYSTEM=polyml-3.1 |
30 ML_SYSTEM=polyml-3.1 |
31 #ML_HOME=/usr/local/ldist/DIR/polyml-3.1/polyml/sunos5.4 |
31 ML_HOME=/usr/local/ldist/DIR/polyml-3.1/polyml/sunos5.4 |
32 #ML_OPTIONS="-h 30000" |
32 ML_OPTIONS="-h 30000" |
33 #LM_LICENSE_FILE=$ML_HOME/license.dat |
33 LM_LICENSE_FILE=$ML_HOME/license.dat |
34 |
34 |
35 # Standard ML of New Jersey 0.93 |
35 # Standard ML of New Jersey 0.93 |
36 #ML_SYSTEM=smlnj-0.93 |
36 #ML_SYSTEM=smlnj-0.93 |
37 #ML_HOME=/usr/local/ldist/DIR/sml-0.93/src |
37 #ML_HOME=/usr/local/ldist/DIR/sml-0.93/src |
38 #ML_OPTIONS="" |
38 #ML_OPTIONS="" |