Contents: suppress comments;
authorwenzelm
Mon Jan 17 15:02:18 2000 +0100 (2000-01-17)
changeset 8130b077b79061b6
parent 8129 29e239c7b8c2
child 8131 f0d47b685433
Contents: suppress comments;
lib/Tools/doc
     1.1 --- a/lib/Tools/doc	Mon Jan 17 14:10:32 2000 +0100
     1.2 +++ b/lib/Tools/doc	Mon Jan 17 15:02:18 2000 +0100
     1.3 @@ -39,7 +39,7 @@
     1.4  if [ -z "$DOC" ]; then
     1.5    for DIR in $DOCS
     1.6    do
     1.7 -    [ -f $DIR/Contents ] && cat $DIR/Contents
     1.8 +    [ -f $DIR/Contents ] && grep -v "^>>" $DIR/Contents
     1.9    done
    1.10  else
    1.11    for DIR in $DOCS