author | wenzelm |
Tue, 27 Sep 2011 00:03:11 +0200 | |
changeset 45094 | a43694a0b726 |
parent 45093 | 26f94c72f306 |
child 45095 | bf7a8906c0cb |
--- 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