| changeset 67581 | 30f412d1d7c3 |
| parent 67099 | 3345d53e7c58 |
| child 69704 | 3fb94d9b87b0 |
| 67580:eb64467e8bcf | 67581:30f412d1d7c3 |
|---|---|
34 |
34 |
35 for PLATFORM in $PLATFORMS |
35 for PLATFORM in $PLATFORMS |
36 do |
36 do |
37 if [ -z "$ML_HOME" ] |
37 if [ -z "$ML_HOME" ] |
38 then |
38 then |
39 if "$POLYML_HOME/$PLATFORM/polyi" -v </dev/null >/dev/null 2>/dev/null |
39 if "$POLYML_HOME/$PLATFORM/poly" -v </dev/null >/dev/null 2>/dev/null |
40 then |
40 then |
41 |
41 |
42 # ML settings |
42 # ML settings |
43 |
43 |
44 ML_SYSTEM=polyml-5.7.1 |
44 ML_SYSTEM=polyml-5.7.1 |