removed --version which is not a valid polyml flag and has no effect
authorgagern
Wed Apr 27 23:04:50 2005 +0200 (2005-04-27)
changeset 15865222092a48131
parent 15864 cc1b4a289321
child 15866 f011452b2815
removed --version which is not a valid polyml flag and has no effect
etc/settings
     1.1 --- a/etc/settings	Wed Apr 27 23:02:08 2005 +0200
     1.2 +++ b/etc/settings	Wed Apr 27 23:04:50 2005 +0200
     1.3 @@ -34,7 +34,7 @@
     1.4    # Poly/ML 4.0, 4.1, 4.1.x
     1.5    # include version number, needed for choosing right options
     1.6    # If automatic setting doesn't work, use e.g. ML_VERSION=4.1.3
     1.7 -  ML_VERSION=$(echo "OS.Process.exit OS.Process.success;" | /usr/bin/poly --version  | sed -n 's,.*Poly/ML[ ]*\([^ ]*\)[ ]*Release,\1,p')
     1.8 +  ML_VERSION=$(echo "OS.Process.exit OS.Process.success;" | /usr/bin/poly | sed -n 's,.*Poly/ML[ ]*\([^ ]*\)[ ]*Release,\1,p')
     1.9    ML_SYSTEM=polyml-${ML_VERSION}
    1.10    # processor/OS type
    1.11    ML_PLATFORM=x86-linux