equal
deleted
inserted
replaced
25 "/usr/local/polyml/$ML_PLATFORM" \ |
25 "/usr/local/polyml/$ML_PLATFORM" \ |
26 "/usr/share/polyml/$ML_PLATFORM" \ |
26 "/usr/share/polyml/$ML_PLATFORM" \ |
27 "/opt/polyml/$ML_PLATFORM" \ |
27 "/opt/polyml/$ML_PLATFORM" \ |
28 $POLY_HOME) |
28 $POLY_HOME) |
29 ML_SYSTEM=$("$ISABELLE_HOME/lib/scripts/polyml-version") |
29 ML_SYSTEM=$("$ISABELLE_HOME/lib/scripts/polyml-version") |
30 ML_OPTIONS="-H 500" |
30 ML_OPTIONS="-H 200" |
31 ML_DBASE="" |
31 ML_DBASE="" |
32 |
32 |
33 # Poly/ML 5.1 |
33 # Poly/ML 5.1 |
34 #ML_PLATFORM=x86-linux |
34 #ML_PLATFORM=x86-linux |
35 #ML_HOME=/usr/local/polyml/x86-linux |
35 #ML_HOME=/usr/local/polyml/x86-linux |