lib/scripts/getsettings
changeset 45094 a43694a0b726
parent 43519 024bd7f5ee0f
child 46741 a29006291f2b
     1.1 --- a/lib/scripts/getsettings	Mon Sep 26 23:51:59 2011 +0200
     1.2 +++ b/lib/scripts/getsettings	Tue Sep 27 00:03:11 2011 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4  export ISABELLE_HOME
     1.5  if { echo -n "$ISABELLE_HOME" | fgrep " " >/dev/null; }
     1.6  then
     1.7 -  echo 1>&2 "### White space in ISABELLE_HOME may cause strange problems later on!"
     1.8 +  echo 1>&2 "### White space in ISABELLE_HOME may cause strange problems!"
     1.9    echo 1>&2 "### ISABELLE_HOME=\"$ISABELLE_HOME\""
    1.10  fi
    1.11