diff -r 7476665f3e0f -r 6e739225dd8a etc/components
--- a/etc/components	Mon Aug 13 20:31:24 2012 +0200
+++ b/etc/components	Tue Aug 14 10:44:03 2012 +0200
@@ -10,6 +10,7 @@
 src/LCF
 src/Sequents
 #misc components
+doc-src
 src/Tools/Code
 src/Tools/jEdit
 src/Tools/WWW_Find