lib/Tools/doc
changeset 8130 b077b79061b6
parent 3173 0013af1bc2c4
child 9788 df671fa2562a
     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