tuned;
authorwenzelm
Tue, 21 Nov 2000 19:02:07 +0100
changeset 10503 c9d087e4a5e8
parent 10502 470d06cc191a
child 10504 d7f5607fbadf
tuned;
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