author | wenzelm |
Fri, 11 Sep 2015 21:44:39 +0200 | |
changeset 61161 | 8fbab2f3433f |
parent 61160 | 12a72ca8329d |
child 61162 | 61908914d191 |
--- a/Admin/polyml/settings Fri Sep 11 21:27:23 2015 +0200 +++ b/Admin/polyml/settings Fri Sep 11 21:44:39 2015 +0200 @@ -36,7 +36,7 @@ do if [ -z "$ML_HOME" ] then - if "$POLYML_HOME/$PLATFORM/polyml" -v >/dev/null 2>/dev/null + if "$POLYML_HOME/$PLATFORM/polyml" -v </dev/null >/dev/null 2>/dev/null then # ML settings