changeset 41759 | 6aa5804aaf90 |
parent 41758 | a231e6110f9b |
child 41760 | bf49b7a85936 |
--- 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