| changeset 45094 | a43694a0b726 |
| parent 43519 | 024bd7f5ee0f |
| child 46741 | a29006291f2b |
--- 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