equal
deleted
inserted
replaced
39 if "$POLYML_HOME/$PLATFORM/polyml" -v </dev/null >/dev/null 2>/dev/null |
39 if "$POLYML_HOME/$PLATFORM/polyml" -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.5.3 |
44 ML_SYSTEM=polyml-5.6 |
45 ML_PLATFORM="$PLATFORM" |
45 ML_PLATFORM="$PLATFORM" |
46 ML_HOME="$POLYML_HOME/$ML_PLATFORM" |
46 ML_HOME="$POLYML_HOME/$ML_PLATFORM" |
47 ML_SOURCES="$POLYML_HOME/src" |
47 ML_SOURCES="$POLYML_HOME/src" |
48 |
48 |
49 case "$ML_PLATFORM" in |
49 case "$ML_PLATFORM" in |