# HG changeset patch
# User wenzelm
# Date 974829727 -3600
# Node ID c9d087e4a5e8aacafedfbcb3d9122c77c9626bed
# Parent  470d06cc191abc8c48f5fdb192d6173e1970d8b6
tuned;

diff -r 470d06cc191a -r c9d087e4a5e8 etc/settings
--- a/etc/settings	Tue Nov 21 16:25:32 2000 +0100
+++ b/etc/settings	Tue Nov 21 19:02:07 2000 +0100
@@ -1,4 +1,4 @@
-#
+# -*- shell-script -*-
 # $Id$
 # Author: Markus Wenzel, TU Muenchen
 # License: GPL (GNU GENERAL PUBLIC LICENSE)
@@ -31,7 +31,7 @@
     "/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_PLATFORM=$("$POLYML_HOME/bin/polyml-platform" 2>/dev/null || echo unknown-platform)
   ML_HOME="$POLYML_HOME/$ML_PLATFORM"
   ML_OPTIONS="-h 30000"
 fi