changeset 67581 | 30f412d1d7c3 |
parent 67099 | 3345d53e7c58 |
child 69704 | 3fb94d9b87b0 |
--- a/Admin/polyml/settings Fri Feb 09 11:14:13 2018 +0100 +++ b/Admin/polyml/settings Fri Feb 09 11:47:18 2018 +0100 @@ -36,7 +36,7 @@ do if [ -z "$ML_HOME" ] then - if "$POLYML_HOME/$PLATFORM/polyi" -v </dev/null >/dev/null 2>/dev/null + if "$POLYML_HOME/$PLATFORM/poly" -v </dev/null >/dev/null 2>/dev/null then # ML settings