changeset 61161 | 8fbab2f3433f |
parent 61158 | ea6a4c8bc722 |
child 61740 | d7e0315fe423 |
--- 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