warn for spaces in ISABELLE_HOME;

--- a/lib/scripts/getsettings	Thu Dec 27 16:43:56 2001 +0100
+++ b/lib/scripts/getsettings	Thu Dec 27 16:44:29 2001 +0100
@@ -15,6 +15,11 @@
 
 #normalize ISABELLE_HOME as passed by caller
 ISABELLE_HOME=$(cd "$ISABELLE_HOME"; echo "$PWD")
+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 "### ISABELLE_HOME=\"$ISABELLE_HOME\""
+fi
 
 #key executables
 ISABELLE="$ISABELLE_HOME/bin/isabelle-process"