| changeset 48725 | e852f4d6af80 |
| parent 48551 | 1f20dfc22000 |
| child 48790 | 6e739225dd8a |
--- a/lib/scripts/getsettings Wed Aug 08 10:40:52 2012 +0200 +++ b/lib/scripts/getsettings Wed Aug 08 10:56:37 2012 +0200 @@ -198,6 +198,7 @@ #main components init_component "$ISABELLE_HOME" [ -d "$ISABELLE_HOME/doc-src" ] && init_component "$ISABELLE_HOME/doc-src" +[ -d "$ISABELLE_HOME/Admin" ] && init_component "$ISABELLE_HOME/Admin" [ -d "$ISABELLE_HOME_USER" ] && init_component "$ISABELLE_HOME_USER" #ML system identifier