1.1 --- a/lib/scripts/getsettings	Thu Dec 27 16:43:56 2001 +0100
     1.2 +++ b/lib/scripts/getsettings	Thu Dec 27 16:44:29 2001 +0100
     1.3 @@ -15,6 +15,11 @@
     1.4  
     1.5  #normalize ISABELLE_HOME as passed by caller
     1.6  ISABELLE_HOME=$(cd "$ISABELLE_HOME"; echo "$PWD")
     1.7 +if { echo -n "$ISABELLE_HOME" | fgrep " " >/dev/null; }
     1.8 +then
     1.9 +  echo 1>&2 "### White space in ISABELLE_HOME may cause strange problems later on!"
    1.10 +  echo 1>&2 "### ISABELLE_HOME=\"$ISABELLE_HOME\""
    1.11 +fi
    1.12  
    1.13  #key executables
    1.14  ISABELLE="$ISABELLE_HOME/bin/isabelle-process"