changeset 64544 | d23b7c9b9dd4 |
parent 61740 | d7e0315fe423 |
child 66691 | a8703e8ee1d3 |
--- a/Admin/polyml/settings Thu Dec 08 17:22:51 2016 +0100 +++ b/Admin/polyml/settings Sat Dec 10 15:45:16 2016 +0100 @@ -36,12 +36,12 @@ do if [ -z "$ML_HOME" ] then - if "$POLYML_HOME/$PLATFORM/polyml" -v </dev/null >/dev/null 2>/dev/null + if "$POLYML_HOME/$PLATFORM/polyi" -v </dev/null >/dev/null 2>/dev/null then # ML settings - ML_SYSTEM=polyml-5.6 + ML_SYSTEM=polyml-5.7 ML_PLATFORM="$PLATFORM" ML_HOME="$POLYML_HOME/$ML_PLATFORM" ML_SOURCES="$POLYML_HOME/src"