1.1 --- a/etc/settings	Tue Nov 21 16:25:32 2000 +0100
     1.2 +++ b/etc/settings	Tue Nov 21 19:02:07 2000 +0100
     1.3 @@ -1,4 +1,4 @@
     1.4 -#
     1.5 +# -*- shell-script -*-
     1.6  # $Id$
     1.7  # Author: Markus Wenzel, TU Muenchen
     1.8  # License: GPL (GNU GENERAL PUBLIC LICENSE)
     1.9 @@ -31,7 +31,7 @@
    1.10      "/usr/local/polyml" \
    1.11      "/opt/polyml")
    1.12    ML_SYSTEM=$("$POLYML_HOME/bin/polyml-version" 2>/dev/null || echo polyml)
    1.13 -  ML_PLATFORM=$("$POLYML_HOME/bin/polyml-platform" 2>/dev/null || echo platform)
    1.14 +  ML_PLATFORM=$("$POLYML_HOME/bin/polyml-platform" 2>/dev/null || echo unknown-platform)
    1.15    ML_HOME="$POLYML_HOME/$ML_PLATFORM"
    1.16    ML_OPTIONS="-h 30000"
    1.17  fi