lib/scripts/getsettings
changeset 48551 1f20dfc22000
parent 48495 bf5b45870110
child 48725 e852f4d6af80
     1.1 --- a/lib/scripts/getsettings	Fri Jul 27 14:22:32 2012 +0200
     1.2 +++ b/lib/scripts/getsettings	Fri Jul 27 15:37:28 2012 +0200
     1.3 @@ -197,6 +197,7 @@
     1.4  
     1.5  #main components
     1.6  init_component "$ISABELLE_HOME"
     1.7 +[ -d "$ISABELLE_HOME/doc-src" ] && init_component "$ISABELLE_HOME/doc-src"
     1.8  [ -d "$ISABELLE_HOME_USER" ] && init_component "$ISABELLE_HOME_USER"
     1.9  
    1.10  #ML system identifier