diff -r 05c13f5a515d -r 57fb9d1ee34a etc/settings
--- a/etc/settings	Mon Jan 21 15:28:34 2002 +0100
+++ b/etc/settings	Mon Jan 21 15:29:06 2002 +0100
@@ -14,10 +14,10 @@
 # binaries.  Do not invent new ML system names unless you know what
 # you are doing.  Only one of the sections below should be activated.
 
-# Poly/ML 3.x, 4.0, 4.1, and 4.1.1
+# Poly/ML 3.x, 4.0, 4.1, 4.1.1, 4.1.2
 if [ -e /usr/bin/poly -a -e /usr/lib/poly ]; then
-  #maybe a shrink-wrapped polyml-4.1.1 on x86-linux ...
-  ML_SYSTEM=polyml-4.1.1
+  #maybe a shrink-wrapped polyml-4.1.2 on x86-linux ...
+  ML_SYSTEM=polyml-4.1.2
   ML_PLATFORM=x86-linux
   ML_HOME=/usr/bin
   ML_DBASE=/usr/lib/poly/ML_dbase