1.1 --- a/etc/settings	Thu Oct 12 17:39:47 2000 +0200
     1.2 +++ b/etc/settings	Thu Oct 12 17:47:32 2000 +0200
     1.3 @@ -14,17 +14,27 @@
     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 or later
     1.8 -POLYML_HOME=$(choosefrom \
     1.9 -  "$ISABELLE_HOME/contrib/polyml" \
    1.10 -  "$ISABELLE_HOME/../polyml" \
    1.11 -  "/usr/share/polyml" \
    1.12 -  "/usr/local/polyml" \
    1.13 -  "/opt/polyml")
    1.14 -ML_SYSTEM=$("$POLYML_HOME/bin/polyml-version" 2>/dev/null || echo polyml)
    1.15 -ML_PLATFORM=$("$POLYML_HOME/bin/polyml-platform" 2>/dev/null)
    1.16 -ML_HOME="$POLYML_HOME/$ML_PLATFORM"
    1.17 -ML_OPTIONS="-h 30000"
    1.18 +# Poly/ML 3.x and 4.0
    1.19 +if [ -e /usr/bin/poly -a -e /usr/lib/poly ]; then
    1.20 +  #maybe a shrink-wrapped polyml-4.0 on x86-linux ...
    1.21 +  ML_SYSTEM=polyml-4.0
    1.22 +  ML_PLATFORM=x86-linux
    1.23 +  ML_HOME=/usr/bin
    1.24 +  ML_DBASE=/usr/lib/poly/ML_dbase
    1.25 +  ML_OPTIONS="-h 30000"
    1.26 +else
    1.27 +  #... or rather a self-contained multi-platform installation
    1.28 +  POLYML_HOME=$(choosefrom \
    1.29 +    "$ISABELLE_HOME/contrib/polyml" \
    1.30 +    "$ISABELLE_HOME/../polyml" \
    1.31 +    "/usr/share/polyml" \
    1.32 +    "/usr/local/polyml" \
    1.33 +    "/opt/polyml")
    1.34 +  ML_SYSTEM=$("$POLYML_HOME/bin/polyml-version" 2>/dev/null || echo polyml)
    1.35 +  ML_PLATFORM=$("$POLYML_HOME/bin/polyml-platform" 2>/dev/null || echo platform)
    1.36 +  ML_HOME="$POLYML_HOME/$ML_PLATFORM"
    1.37 +  ML_OPTIONS="-h 30000"
    1.38 +fi
    1.39  
    1.40  # Standard ML of New Jersey 110 or later
    1.41  #ML_SYSTEM=smlnj-110