# HG changeset patch
# User wenzelm
# Date 1249385733 -7200
# Node ID 13920dbe4547551e1418957b63664c6253d948b7
# Parent  8175fda90c46042d6f82f676b5c95671f9a8b495
more uniform handling of ISABELLE_HOME_USER component;
discontinued ISABELLE_IGNORE_USER_SETTINGS (ever used? cf. c567f9fd61a2);

diff -r 8175fda90c46 -r 13920dbe4547 lib/scripts/getsettings
--- a/lib/scripts/getsettings	Tue Aug 04 13:29:52 2009 +0200
+++ b/lib/scripts/getsettings	Tue Aug 04 13:35:33 2009 +0200
@@ -102,9 +102,8 @@
 init_component "$ISABELLE_HOME"
 
 [ "$ISABELLE_HOME" -ef "$ISABELLE_HOME_USER" ] && \
-  { echo >&2 "### ISABELLE_HOME and ISABELLE_HOME_USER should not be the same directory!"; }
-[ -z "$ISABELLE_IGNORE_USER_SETTINGS" -a -f "$ISABELLE_HOME_USER/etc/settings" ] && \
-  init_component "$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
 if [ -z "$ML_PLATFORM" ]; then