diff -r 26f94c72f306 -r a43694a0b726 lib/scripts/getsettings
--- a/lib/scripts/getsettings	Mon Sep 26 23:51:59 2011 +0200
+++ b/lib/scripts/getsettings	Tue Sep 27 00:03:11 2011 +0200
@@ -14,7 +14,7 @@
 export ISABELLE_HOME
 if { echo -n "$ISABELLE_HOME" | fgrep " " >/dev/null; }
 then
-  echo 1>&2 "### White space in ISABELLE_HOME may cause strange problems later on!"
+  echo 1>&2 "### White space in ISABELLE_HOME may cause strange problems!"
   echo 1>&2 "### ISABELLE_HOME=\"$ISABELLE_HOME\""
 fi