author | wenzelm |
Fri, 27 Jul 2012 15:37:28 +0200 | |
changeset 48551 | 1f20dfc22000 |
parent 48550 | 97592027a2a8 |
child 48552 | b1819875b76a |
--- a/lib/scripts/getsettings Fri Jul 27 14:22:32 2012 +0200 +++ b/lib/scripts/getsettings Fri Jul 27 15:37:28 2012 +0200 @@ -197,6 +197,7 @@ #main components init_component "$ISABELLE_HOME" +[ -d "$ISABELLE_HOME/doc-src" ] && init_component "$ISABELLE_HOME/doc-src" [ -d "$ISABELLE_HOME_USER" ] && init_component "$ISABELLE_HOME_USER" #ML system identifier