--- a/lib/scripts/getsettings Fri Aug 17 11:37:14 2012 +0200
+++ b/lib/scripts/getsettings Fri Aug 17 11:42:05 2012 +0200
@@ -34,11 +34,6 @@
fi
export ISABELLE_HOME
-if { echo -n "$ISABELLE_HOME" | fgrep " " >/dev/null; }
-then
- echo 1>&2 "### White space in ISABELLE_HOME may cause strange problems!"
- echo 1>&2 "### ISABELLE_HOME=\"$ISABELLE_HOME\""
-fi
#key executables
ISABELLE_PROCESS="$ISABELLE_HOME/bin/isabelle-process"
@@ -58,7 +53,7 @@
#Isabelle distribution identifier -- filled in automatically!
ISABELLE_ID=""
-ISABELLE_IDENTIFIER=""
+[ -z "$ISABELLE_IDENTIFIER" ] && ISABELLE_IDENTIFIER=""
#sometimes users put strange things in here ...
unset ENV