# HG changeset patch
# User wenzelm
# Date 1343396248 -7200
# Node ID 1f20dfc220009d9a3d6bdfb4ad80a0f17c6617c3
# Parent  97592027a2a8e96cea8df229a7de647c8b484bec
include doc-src as component, and thus its sessions defined in ROOT;

diff -r 97592027a2a8 -r 1f20dfc22000 lib/scripts/getsettings
--- 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