more uniform handling of ISABELLE_HOME_USER component;
authorwenzelm
Tue Aug 04 13:35:33 2009 +0200 (2009-08-04)
changeset 3232113920dbe4547
parent 32320 8175fda90c46
child 32322 45cb4a86eca2
more uniform handling of ISABELLE_HOME_USER component;
discontinued ISABELLE_IGNORE_USER_SETTINGS (ever used? cf. c567f9fd61a2);
lib/scripts/getsettings
     1.1 --- a/lib/scripts/getsettings	Tue Aug 04 13:29:52 2009 +0200
     1.2 +++ b/lib/scripts/getsettings	Tue Aug 04 13:35:33 2009 +0200
     1.3 @@ -102,9 +102,8 @@
     1.4  init_component "$ISABELLE_HOME"
     1.5  
     1.6  [ "$ISABELLE_HOME" -ef "$ISABELLE_HOME_USER" ] && \
     1.7 -  { echo >&2 "### ISABELLE_HOME and ISABELLE_HOME_USER should not be the same directory!"; }
     1.8 -[ -z "$ISABELLE_IGNORE_USER_SETTINGS" -a -f "$ISABELLE_HOME_USER/etc/settings" ] && \
     1.9 -  init_component "$ISABELLE_HOME_USER"
    1.10 +  { echo >&2 "### ISABELLE_HOME and ISABELLE_HOME_USER must not be the same directory!"; }
    1.11 +[ -d "$ISABELLE_HOME_USER" ] && init_component "$ISABELLE_HOME_USER"
    1.12  
    1.13  #ML system identifier
    1.14  if [ -z "$ML_PLATFORM" ]; then