Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
more uniform handling of ISABELLE_HOME_USER component;
authorwenzelm
Tue, 04 Aug 2009 13:35:33 +0200
changeset 32321 13920dbe4547
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 file | annotate | diff | comparison | revisions 
--- 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
isabelle