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