equal
deleted
inserted
replaced
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/share/smlnj/bin |
16 ML_HOME=/usr/share/smlnj/bin |
17 ML_OPTIONS="@SMLdebug=/dev/null" |
17 ML_OPTIONS="@SMLdebug=/dev/null" |
18 ML_PLATFORM=$(eval $($ML_HOME/.arch-n-opsys); echo $HEAP_SUFFIX) |
18 ML_PLATFORM=$(eval $($ML_HOME/.arch-n-opsys 2>/dev/null); echo $HEAP_SUFFIX) |
19 |
19 |
20 # MLWorks 2.0 or later |
20 # MLWorks 2.0 or later |
21 #ML_SYSTEM=mlworks |
21 #ML_SYSTEM=mlworks |
22 #ML_HOME=/usr/local/mlworks/bin |
22 #ML_HOME=/usr/local/mlworks/bin |
23 #ML_OPTIONS="" |
23 #ML_OPTIONS="" |