# HG changeset patch
# User wenzelm
# Date 1009467869 -3600
# Node ID fa556d3fe5f2b36f18aa1a48445dd6ad94d48146
# Parent  14822e4436bfd45b23e2af29a923e10da3aaa830
warn for spaces in ISABELLE_HOME;

diff -r 14822e4436bf -r fa556d3fe5f2 lib/scripts/getsettings
--- 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"