--- 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"