# HG changeset patch # User kleing # Date 1078802381 -3600 # Node ID 5b61dc4eab24466126729a310032818fcceffb6b # Parent 0bc2519e9990330b9739a123a6afe7cdce025073 include more explanation of variables diff -r 0bc2519e9990 -r 5b61dc4eab24 etc/settings --- 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