lib/scripts/getsettings

--- a/lib/scripts/getsettings	Mon Feb 17 11:04:00 1997 +0100
+++ b/lib/scripts/getsettings	Mon Feb 17 12:00:00 1997 +0100
@@ -9,7 +9,7 @@
 
 set -o allexport
 
-#users tend to put strange things in here
+#users tend to put strange things in here ...
 unset ENV
 unset BASH_ENV
 
@@ -18,6 +18,7 @@
 unset OSTYPE
 PLATFORM=$(bash -norc -c 'echo $HOSTTYPE-$OSTYPE')
 
+#get actual settings
 . $ISABELLE_HOME/etc/settings || exit 2
 [ -f $ISABELLE_HOME_USER/etc/settings ] && . $ISABELLE_HOME_USER/etc/settings