--- a/etc/settings Thu Oct 12 17:39:47 2000 +0200
+++ b/etc/settings Thu Oct 12 17:47:32 2000 +0200
@@ -14,17 +14,27 @@
# 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 or later
-POLYML_HOME=$(choosefrom \
- "$ISABELLE_HOME/contrib/polyml" \
- "$ISABELLE_HOME/../polyml" \
- "/usr/share/polyml" \
- "/usr/local/polyml" \
- "/opt/polyml")
-ML_SYSTEM=$("$POLYML_HOME/bin/polyml-version" 2>/dev/null || echo polyml)
-ML_PLATFORM=$("$POLYML_HOME/bin/polyml-platform" 2>/dev/null)
-ML_HOME="$POLYML_HOME/$ML_PLATFORM"
-ML_OPTIONS="-h 30000"
+# Poly/ML 3.x and 4.0
+if [ -e /usr/bin/poly -a -e /usr/lib/poly ]; then
+ #maybe a shrink-wrapped polyml-4.0 on x86-linux ...
+ ML_SYSTEM=polyml-4.0
+ ML_PLATFORM=x86-linux
+ ML_HOME=/usr/bin
+ ML_DBASE=/usr/lib/poly/ML_dbase
+ ML_OPTIONS="-h 30000"
+else
+ #... or rather a self-contained multi-platform installation
+ POLYML_HOME=$(choosefrom \
+ "$ISABELLE_HOME/contrib/polyml" \
+ "$ISABELLE_HOME/../polyml" \
+ "/usr/share/polyml" \
+ "/usr/local/polyml" \
+ "/opt/polyml")
+ ML_SYSTEM=$("$POLYML_HOME/bin/polyml-version" 2>/dev/null || echo polyml)
+ ML_PLATFORM=$("$POLYML_HOME/bin/polyml-platform" 2>/dev/null || echo platform)
+ ML_HOME="$POLYML_HOME/$ML_PLATFORM"
+ ML_OPTIONS="-h 30000"
+fi
# Standard ML of New Jersey 110 or later
#ML_SYSTEM=smlnj-110