equal
deleted
inserted
replaced
12 |
12 |
13 # Note that ML_HOME specifies the location of the actual compiler |
13 # Note that ML_HOME specifies the location of the actual compiler |
14 # binaries. Do not invent new ML system names unless you know what |
14 # binaries. Do not invent new ML system names unless you know what |
15 # you are doing. |
15 # you are doing. |
16 |
16 |
17 # Poly/ML 3.x |
17 # Poly/ML 3.x or later |
18 POLYML_HOME=$(choosefrom \ |
18 POLYML_HOME=$(choosefrom \ |
19 "$ISABELLE_HOME/contrib/polyml" \ |
19 "$ISABELLE_HOME/contrib/polyml" \ |
20 "$ISABELLE_HOME/../polyml") |
20 "$ISABELLE_HOME/../polyml") |
21 ML_PLATFORM=$($POLYML_HOME/bin/polyml-platform 2>/dev/null) |
21 ML_PLATFORM=$($POLYML_HOME/bin/polyml-platform 2>/dev/null) |
22 ML_HOME=$POLYML_HOME/$ML_PLATFORM |
22 ML_HOME=$POLYML_HOME/$ML_PLATFORM |
23 ML_SYSTEM=polyml-3.x |
23 ML_SYSTEM=$($POLYML_HOME/bin/polyml-version 2>/dev/null) |
24 ML_OPTIONS="-h 30000" |
24 ML_OPTIONS="-h 30000" |
25 |
25 |
26 # Standard ML of New Jersey 110 or later |
26 # Standard ML of New Jersey 110 or later |
27 #ML_SYSTEM=smlnj-110 |
27 #ML_SYSTEM=smlnj-110 |
28 #ML_HOME=$ISABELLE_HOME/../smlnj/bin |
28 #ML_HOME=$ISABELLE_HOME/../smlnj/bin |