eliminated somewhat obsolete warning -- former "$HOME/Isabelle" vs. "$HOME/isabelle" no longer exist;

--- a/lib/scripts/getsettings	Sun Feb 13 17:19:43 2011 +0100
+++ b/lib/scripts/getsettings	Sun Feb 13 17:29:44 2011 +0100
@@ -152,9 +152,6 @@
 
 #main components
 init_component "$ISABELLE_HOME"
-
-[ "$ISABELLE_HOME" -ef "$ISABELLE_HOME_USER" ] && \
-  { echo >&2 "### ISABELLE_HOME and ISABELLE_HOME_USER must not be the same directory!"; }
 [ -d "$ISABELLE_HOME_USER" ] && init_component "$ISABELLE_HOME_USER"
 
 #ML system identifier