doc/*.html
doc/*.txt
doc/*.dvi