# HG changeset patch
# User wenzelm
# Date 1297614584 -3600
# Node ID 6aa5804aaf9024154a4cc521256d2672038583de
# Parent  a231e6110f9bba73e6652b74c0787654494e96b4
eliminated somewhat obsolete warning -- former "$HOME/Isabelle" vs. "$HOME/isabelle" no longer exist;

diff -r a231e6110f9b -r 6aa5804aaf90 lib/scripts/getsettings
--- 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