--- 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