# HG changeset patch
# User aspinall
# Date 1113499857 -7200
# Node ID 56a807868e236e9d16e919015805ccd7a1730864
# Parent  75b9219980d3018c5860a1a779d30f09ea813d3f
Include automatic determination of poly version.

diff -r 75b9219980d3 -r 56a807868e23 etc/settings
--- a/etc/settings	Thu Apr 14 19:16:07 2005 +0200
+++ b/etc/settings	Thu Apr 14 19:30:57 2005 +0200
@@ -33,7 +33,9 @@
 
   # Poly/ML 4.0, 4.1, 4.1.x
   # include version number, needed for choosing right options
-  ML_SYSTEM=polyml-4.1.3    
+  # 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_SYSTEM=polyml-${ML_VERSION}
   # processor/OS type
   ML_PLATFORM=x86-linux
   # where to find binaries