1.1 --- a/etc/settings	Thu Mar 11 00:15:24 2004 +0100
     1.2 +++ b/etc/settings	Thu Mar 11 03:53:43 2004 +0100
     1.3 @@ -14,10 +14,25 @@
     1.4  # binaries.  Do not invent new ML system names unless you know what
     1.5  # you are doing.  Only one of the sections below should be activated.
     1.6  
     1.7 -# Poly/ML 3.x, 4.0, 4.1, 4.1.1, 4.1.2
     1.8 -if [ -e /usr/bin/poly -a -e /usr/lib/poly ]; then
     1.9 -  #maybe a shrink-wrapped polyml on x86-linux ...
    1.10  
    1.11 +# try finding the poly packages from the Isabelle site in the usual places
    1.12 +POLYML_HOME=$(choosefrom \
    1.13 +  "$ISABELLE_HOME/contrib/polyml" \
    1.14 +  "$ISABELLE_HOME/../polyml" \
    1.15 +  "/usr/share/polyml" \
    1.16 +  "/usr/local/polyml" \
    1.17 +  "/opt/polyml")
    1.18 +
    1.19 +if [ -n "$POLYML_HOME" -a -e "$POLYML_HOME/bin/polyml-version" ]; then
    1.20 +  # looks like Isabelle poly packages
    1.21 +  ML_SYSTEM=$("$POLYML_HOME/bin/polyml-version" 2>/dev/null || echo polyml)
    1.22 +  ML_PLATFORM=$("$POLYML_HOME/bin/polyml-platform" 2>/dev/null || echo unknown-platform)
    1.23 +  ML_HOME="$POLYML_HOME/$ML_PLATFORM"
    1.24 +  ML_OPTIONS="-h 15000"
    1.25 +elif [ -e /usr/bin/poly -a -e /usr/lib/poly ]; then
    1.26 +  # maybe a shrink-wrapped polyml on x86-linux ...
    1.27 +
    1.28 +  # Poly/ML 3.x, 4.0, 4.1, 4.1.x
    1.29    # include version number, needed for choosing right options
    1.30    ML_SYSTEM=polyml-4.1.3    
    1.31    # processor/OS type
    1.32 @@ -28,18 +43,6 @@
    1.33    ML_DBASE=/usr/lib/poly/ML_dbase
    1.34    # options to pass to poly
    1.35    ML_OPTIONS="-h 15000"
    1.36 -else
    1.37 -  #... or rather a self-contained multi-platform installation
    1.38 -  POLYML_HOME=$(choosefrom \
    1.39 -    "$ISABELLE_HOME/contrib/polyml" \
    1.40 -    "$ISABELLE_HOME/../polyml" \
    1.41 -    "/usr/share/polyml" \
    1.42 -    "/usr/local/polyml" \
    1.43 -    "/opt/polyml")
    1.44 -  ML_SYSTEM=$("$POLYML_HOME/bin/polyml-version" 2>/dev/null || echo polyml)
    1.45 -  ML_PLATFORM=$("$POLYML_HOME/bin/polyml-platform" 2>/dev/null || echo unknown-platform)
    1.46 -  ML_HOME="$POLYML_HOME/$ML_PLATFORM"
    1.47 -  ML_OPTIONS="-h 15000"
    1.48  fi
    1.49  
    1.50  # Standard ML of New Jersey 110 or later