Admin/polyml/settings
changeset 64544 d23b7c9b9dd4
parent 61740 d7e0315fe423
child 66691 a8703e8ee1d3
     1.1 --- a/Admin/polyml/settings	Mon Nov 23 17:56:11 2015 +0100
     1.2 +++ b/Admin/polyml/settings	Sat Dec 10 15:45:16 2016 +0100
     1.3 @@ -36,12 +36,12 @@
     1.4  do
     1.5    if [ -z "$ML_HOME" ]
     1.6    then
     1.7 -    if "$POLYML_HOME/$PLATFORM/polyml" -v </dev/null >/dev/null 2>/dev/null
     1.8 +    if "$POLYML_HOME/$PLATFORM/polyi" -v </dev/null >/dev/null 2>/dev/null
     1.9      then
    1.10  
    1.11        # ML settings
    1.12  
    1.13 -      ML_SYSTEM=polyml-5.6
    1.14 +      ML_SYSTEM=polyml-5.7
    1.15        ML_PLATFORM="$PLATFORM"
    1.16        ML_HOME="$POLYML_HOME/$ML_PLATFORM"
    1.17        ML_SOURCES="$POLYML_HOME/src"