# HG changeset patch
# User gagern
# Date 1114635890 -7200
# Node ID 222092a48131727823989ec6fcde842c53511ba0
# Parent  cc1b4a289321e7b8b39bbc6527d577cd69a1ecef
removed --version which is not a valid polyml flag and has no effect

diff -r cc1b4a289321 -r 222092a48131 etc/settings
--- a/etc/settings	Wed Apr 27 23:02:08 2005 +0200
+++ b/etc/settings	Wed Apr 27 23:04:50 2005 +0200
@@ -34,7 +34,7 @@
   # Poly/ML 4.0, 4.1, 4.1.x
   # include version number, needed for choosing right options
   # If automatic setting doesn't work, use e.g. ML_VERSION=4.1.3
-  ML_VERSION=$(echo "OS.Process.exit OS.Process.success;" | /usr/bin/poly --version  | sed -n 's,.*Poly/ML[ ]*\([^ ]*\)[ ]*Release,\1,p')
+  ML_VERSION=$(echo "OS.Process.exit OS.Process.success;" | /usr/bin/poly | sed -n 's,.*Poly/ML[ ]*\([^ ]*\)[ ]*Release,\1,p')
   ML_SYSTEM=polyml-${ML_VERSION}
   # processor/OS type
   ML_PLATFORM=x86-linux