# HG changeset patch
# User wenzelm
# Date 856177200 -3600
# Node ID a7f469c0ba592501c9c3f423e7a05fc52604b782
# Parent  3c3a84cc85a90c0e11eb71ad4f1eeba77750d432
tuned comments;

diff -r 3c3a84cc85a9 -r a7f469c0ba59 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