--- 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