equal
deleted
inserted
replaced
43 #ISAMODE_HOME=$ISABELLE_HOME/lib/Isamode |
43 #ISAMODE_HOME=$ISABELLE_HOME/lib/Isamode |
44 |
44 |
45 |
45 |
46 ## ML compilers and options |
46 ## ML compilers and options |
47 |
47 |
48 #ML_SYSTEM=polyml-2.07 |
48 #ML_SYSTEM=polyml-2.x |
49 #ML_HOME=/usr/local/ldist/DIR/polyml/polyml/solaris2 |
49 #ML_HOME=/usr/local/ldist/DIR/polyml/polyml/solaris2 |
50 #ML_OPTIONS="-h 30000" |
50 #ML_OPTIONS="-h 30000" |
51 |
51 |
52 ML_SYSTEM=polyml-3.1 |
52 ML_SYSTEM=polyml-3.1 |
53 ML_HOME=/usr/local/ldist/DIR/polyml-3.1/polyml/sunos5.4 |
53 ML_HOME=/usr/local/ldist/DIR/polyml-3.1/polyml/sunos5.4 |
54 ML_OPTIONS="-h 30000" |
54 ML_OPTIONS="-h 30000" |
55 LM_LICENSE_FILE=$ML_HOME/license.dat |
55 LM_LICENSE_FILE=$ML_HOME/license.dat |
56 |
56 |
57 #ML_SYSTEM=smlnj-0.93 |
57 #ML_SYSTEM=smlnj-0.93 |
|
58 #ML_HOME=/usr/local/ldist/DIR/sml-0.93/src |
|
59 #ML_OPTIONS="" |
58 |
60 |
59 #ML_SYSTEM=smlnj-1.07 |
61 #ML_SYSTEM=smlnj-1.07 |
60 #ML_HOME=/usr/local/sml107 |
62 #ML_HOME=/usr/local/sml107 |
61 #ML_OPTIONS="@SMLdebug=/dev/null" |
63 #ML_OPTIONS="@SMLdebug=/dev/null" |
62 |
64 |