equal
deleted
inserted
replaced
9 ### |
9 ### |
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 # Poly/ML 3.x |
|
15 POLYML_HOME=$ISABELLE_HOME/../polyml |
|
16 ML_PLATFORM=$($POLYML_HOME/bin/polyml-platform 2>/dev/null) |
|
17 ML_HOME=$POLYML_HOME/$ML_PLATFORM |
|
18 ML_SYSTEM=polyml-3.x |
|
19 ML_OPTIONS="-h 30000" |
|
20 |
14 # Standard ML of New Jersey 110 or later |
21 # Standard ML of New Jersey 110 or later |
15 ML_SYSTEM=smlnj-110 |
22 #ML_SYSTEM=smlnj-110 |
16 ML_HOME=$ISABELLE_HOME/../smlnj/bin |
23 #ML_HOME=$ISABELLE_HOME/../smlnj/bin |
17 ML_OPTIONS="@SMLdebug=/dev/null" |
24 #ML_OPTIONS="@SMLdebug=/dev/null" |
18 ML_PLATFORM=$(eval $($ML_HOME/.arch-n-opsys 2>/dev/null); echo $HEAP_SUFFIX) |
25 #ML_PLATFORM=$(eval $($ML_HOME/.arch-n-opsys 2>/dev/null); echo $HEAP_SUFFIX) |
19 |
26 |
20 # MLWorks 2.0 or later |
27 # MLWorks 2.0 or later |
21 #ML_SYSTEM=mlworks |
28 #ML_SYSTEM=mlworks |
22 #ML_HOME=/usr/local/mlworks/bin |
29 #ML_HOME=/usr/local/mlworks/bin |
23 #ML_OPTIONS="" |
30 #ML_OPTIONS="" |
26 # Poly/ML 2.x |
33 # Poly/ML 2.x |
27 #ML_SYSTEM=polyml-2.07 |
34 #ML_SYSTEM=polyml-2.07 |
28 #ML_HOME=/usr/local/ldist/DIR/polyml/polyml/solaris2 |
35 #ML_HOME=/usr/local/ldist/DIR/polyml/polyml/solaris2 |
29 #ML_OPTIONS="-h 30000" |
36 #ML_OPTIONS="-h 30000" |
30 #ML_PLATFORM="" |
37 #ML_PLATFORM="" |
31 |
|
32 # Poly/ML 3.1 |
|
33 #ML_SYSTEM=polyml-3.1 |
|
34 #ML_HOME=/usr/local/ldist/DIR/polyml-3.1/polyml/sunos5.4 |
|
35 #ML_OPTIONS="-h 30000" |
|
36 #ML_PLATFORM="" |
|
37 #LM_LICENSE_FILE=$ML_HOME/license.dat |
|
38 |
38 |
39 # Standard ML of New Jersey 0.93 |
39 # Standard ML of New Jersey 0.93 |
40 #ML_SYSTEM=smlnj-0.93 |
40 #ML_SYSTEM=smlnj-0.93 |
41 #ML_HOME=/usr/local/ldist/DIR/sml-0.93/src |
41 #ML_HOME=/usr/local/ldist/DIR/sml-0.93/src |
42 #ML_OPTIONS="" |
42 #ML_OPTIONS="" |