| changeset 48790 | 6e739225dd8a |
| parent 48725 | e852f4d6af80 |
| child 48837 | d1d806a42c91 |
--- a/lib/scripts/getsettings Mon Aug 13 20:31:24 2012 +0200 +++ b/lib/scripts/getsettings Tue Aug 14 10:44:03 2012 +0200 @@ -197,7 +197,6 @@ #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"