# HG changeset patch
# User wenzelm
# Date 948117738 -3600
# Node ID b077b79061b684bd3675a88263526ad3331ff348
# Parent  29e239c7b8c2be588d595cd7ea6400ddffecda8d
Contents: suppress comments;

diff -r 29e239c7b8c2 -r b077b79061b6 lib/Tools/doc
--- a/lib/Tools/doc	Mon Jan 17 14:10:32 2000 +0100
+++ b/lib/Tools/doc	Mon Jan 17 15:02:18 2000 +0100
@@ -39,7 +39,7 @@
 if [ -z "$DOC" ]; then
   for DIR in $DOCS
   do
-    [ -f $DIR/Contents ] && cat $DIR/Contents
+    [ -f $DIR/Contents ] && grep -v "^>>" $DIR/Contents
   done
 else
   for DIR in $DOCS