equal
deleted
inserted
replaced
32 # maybe a shrink-wrapped polyml on x86-linux ... |
32 # maybe a shrink-wrapped polyml on x86-linux ... |
33 |
33 |
34 # Poly/ML 4.0, 4.1, 4.1.x |
34 # Poly/ML 4.0, 4.1, 4.1.x |
35 # include version number, needed for choosing right options |
35 # include version number, needed for choosing right options |
36 # If automatic setting doesn't work, use e.g. ML_VERSION=4.1.3 |
36 # If automatic setting doesn't work, use e.g. ML_VERSION=4.1.3 |
37 ML_VERSION=$(echo "OS.Process.exit OS.Process.success;" | /usr/bin/poly --version | sed -n 's,Poly/ML[ ]*\([^ ]*\)[ ]*Release,\1,p') |
37 ML_VERSION=$(echo "OS.Process.exit OS.Process.success;" | /usr/bin/poly --version | sed -n 's,.*Poly/ML[ ]*\([^ ]*\)[ ]*Release,\1,p') |
38 ML_SYSTEM=polyml-${ML_VERSION} |
38 ML_SYSTEM=polyml-${ML_VERSION} |
39 # processor/OS type |
39 # processor/OS type |
40 ML_PLATFORM=x86-linux |
40 ML_PLATFORM=x86-linux |
41 # where to find binaries |
41 # where to find binaries |
42 ML_HOME=/usr/bin |
42 ML_HOME=/usr/bin |