equal
deleted
inserted
replaced
30 ML_HOME="$POLYML_HOME/$ML_PLATFORM" |
30 ML_HOME="$POLYML_HOME/$ML_PLATFORM" |
31 ML_OPTIONS="-h 15000" |
31 ML_OPTIONS="-h 15000" |
32 elif [ -e /usr/bin/poly -a -e /usr/lib/poly ]; then |
32 elif [ -e /usr/bin/poly -a -e /usr/lib/poly ]; then |
33 # maybe a shrink-wrapped polyml on x86-linux ... |
33 # maybe a shrink-wrapped polyml on x86-linux ... |
34 |
34 |
35 # Poly/ML 3.x, 4.0, 4.1, 4.1.x |
35 # Poly/ML 4.0, 4.1, 4.1.x |
36 # include version number, needed for choosing right options |
36 # include version number, needed for choosing right options |
37 ML_SYSTEM=polyml-4.1.3 |
37 ML_SYSTEM=polyml-4.1.3 |
38 # processor/OS type |
38 # processor/OS type |
39 ML_PLATFORM=x86-linux |
39 ML_PLATFORM=x86-linux |
40 # where to find binaries |
40 # where to find binaries |