author | wenzelm |
Thu, 15 Sep 2005 17:18:57 +0200 | |
changeset 17419 | 16df5a5eef68 |
parent 17418 | cd5d8b444d6e |
child 17420 | bdcffa8d8665 |
--- a/lib/scripts/polyml-version Thu Sep 15 17:17:06 2005 +0200 +++ b/lib/scripts/polyml-version Thu Sep 15 17:18:57 2005 +0200 @@ -7,6 +7,6 @@ echo -n polyml if [ -x "$ML_HOME/poly" ]; then - "$ML_HOME/poly" -r /dev/null | head -n 1 | \ + "$ML_HOME/poly" -noDisplay -r /dev/null | head -n 1 | \ sed -n 's,^Poly/ML RTS version [^ ]*\(-[^ ]*\).*$,\1,p' fi