| changeset 17419 | 16df5a5eef68 |
| parent 16996 | 32afaa947f6e |
| child 20748 | 4bcf492c6c9d |
--- 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