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="" |
30 # Standard ML of New Jersey 1.07 |
30 # Standard ML of New Jersey 1.07 |
31 #ML_SYSTEM=smlnj-1.07 |
31 #ML_SYSTEM=smlnj-1.07 |
32 #ML_HOME=/usr/local/sml107/bin |
32 #ML_HOME=/usr/local/sml107/bin |
33 #ML_OPTIONS="@SMLdebug=/dev/null" |
33 #ML_OPTIONS="@SMLdebug=/dev/null" |
34 |
34 |
35 # Standard ML of New Jersey 1.09.27, or later |
35 # Standard ML of New Jersey 1.09.27, 1.09.28, or later |
36 #ML_SYSTEM=smlnj-1.09 |
36 ML_SYSTEM=smlnj-1.09 |
37 #ML_HOME=/usr/local/sml109.27/bin |
37 ML_HOME=/usr/local/sml109.27/bin |
38 #ML_OPTIONS="@SMLdebug=/dev/null" |
38 ML_OPTIONS="@SMLdebug=/dev/null" |
39 |
39 |
40 |
40 |
41 ### |
41 ### |
42 ### Compilation options |
42 ### Compilation options |
43 ### |
43 ### |