diff -r 7476665f3e0f -r 6e739225dd8a lib/scripts/getsettings
--- 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"