look for multi platform poly first, choose shrink wrapped poly-4.1.3 (guess) only
authorkleing
Thu, 11 Mar 2004 03:53:43 +0100
changeset 14461 fab539f843d9
parent 14460 04e787a4f17a
child 14462 e6550f190fe9
look for multi platform poly first, choose shrink wrapped poly-4.1.3 (guess) only if no multi platform installation found.
etc/settings
--- a/etc/settings	Thu Mar 11 00:15:24 2004 +0100
+++ b/etc/settings	Thu Mar 11 03:53:43 2004 +0100
@@ -14,10 +14,25 @@
 # 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, 4.1.1, 4.1.2
-if [ -e /usr/bin/poly -a -e /usr/lib/poly ]; then
-  #maybe a shrink-wrapped polyml on x86-linux ...
+
+# try finding the poly packages from the Isabelle site in the usual places
+POLYML_HOME=$(choosefrom \
+  "$ISABELLE_HOME/contrib/polyml" \
+  "$ISABELLE_HOME/../polyml" \
+  "/usr/share/polyml" \
+  "/usr/local/polyml" \
+  "/opt/polyml")
 
+if [ -n "$POLYML_HOME" -a -e "$POLYML_HOME/bin/polyml-version" ]; then
+  # looks like Isabelle poly packages
+  ML_SYSTEM=$("$POLYML_HOME/bin/polyml-version" 2>/dev/null || echo polyml)
+  ML_PLATFORM=$("$POLYML_HOME/bin/polyml-platform" 2>/dev/null || echo unknown-platform)
+  ML_HOME="$POLYML_HOME/$ML_PLATFORM"
+  ML_OPTIONS="-h 15000"
+elif [ -e /usr/bin/poly -a -e /usr/lib/poly ]; then
+  # maybe a shrink-wrapped polyml on x86-linux ...
+
+  # Poly/ML 3.x, 4.0, 4.1, 4.1.x
   # include version number, needed for choosing right options
   ML_SYSTEM=polyml-4.1.3    
   # processor/OS type
@@ -28,18 +43,6 @@
   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
-  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 unknown-platform)
-  ML_HOME="$POLYML_HOME/$ML_PLATFORM"
-  ML_OPTIONS="-h 15000"
 fi
 
 # Standard ML of New Jersey 110 or later