equal
deleted
inserted
replaced
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="" |
29 |
29 |
30 # Standard ML of New Jersey 1.09.27 or later |
30 # Standard ML of New Jersey 109.27 to 109.33 |
31 #ML_SYSTEM=smlnj-1.09 |
31 #ML_SYSTEM=smlnj-109 |
32 #ML_HOME=/usr/local/sml109.27/bin |
32 #ML_HOME=/usr/proj/smlnj/109.32/bin |
|
33 #ML_OPTIONS="@SMLdebug=/dev/null" |
|
34 |
|
35 # Standard ML of New Jersey 110 or later |
|
36 #ML_SYSTEM=smlnj-110 |
|
37 #ML_HOME=/usr/proj/smlnj/110/bin |
33 #ML_OPTIONS="@SMLdebug=/dev/null" |
38 #ML_OPTIONS="@SMLdebug=/dev/null" |
34 |
39 |
35 |
40 |
36 ### |
41 ### |
37 ### Compilation options |
42 ### Compilation options |