etc/settings
changeset 14447 5b61dc4eab24
parent 14344 0f0a2148a099
child 14451 2253d273d944
--- a/etc/settings	Mon Mar 08 12:18:19 2004 +0100
+++ b/etc/settings	Tue Mar 09 04:19:41 2004 +0100
@@ -16,11 +16,17 @@
 
 # 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.2 on x86-linux ...
-  ML_SYSTEM=polyml-4.1.2
+  #maybe a shrink-wrapped polyml on x86-linux ...
+
+  # include version number, needed for choosing right options
+  ML_SYSTEM=polyml-4.1.3    
+  # processor/OS type
   ML_PLATFORM=x86-linux
+  # where to find binaries
   ML_HOME=/usr/bin
+  # where to find the standard database
   ML_DBASE=/usr/lib/poly/ML_dbase
+  # options to pass to poly
   ML_OPTIONS="-h 15000"
 else
   #... or rather a self-contained multi-platform installation