Admin/polyml/settings
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"