changeset 69822 | 8c587dd44f51 |
parent 69704 | 3fb94d9b87b0 |
child 70988 | 38ade730f6df |
69821:8432b771f12e | 69822:8c587dd44f51 |
---|---|
10 else |
10 else |
11 ML_PLATFORM="${ML_PLATFORM/x86_64/x86_64_32}" |
11 ML_PLATFORM="${ML_PLATFORM/x86_64/x86_64_32}" |
12 ML_OPTIONS="--minheap 500" |
12 ML_OPTIONS="--minheap 500" |
13 fi |
13 fi |
14 |
14 |
15 ML_SYSTEM=polyml-5.7.1 |
15 ML_SYSTEM=polyml-5.8 |
16 ML_HOME="$POLYML_HOME/$ML_PLATFORM" |
16 ML_HOME="$POLYML_HOME/$ML_PLATFORM" |
17 ML_SOURCES="$POLYML_HOME/src" |
17 ML_SOURCES="$POLYML_HOME/src" |