echo the filename to stderr for 'make dok-tidy'

echo the filename to stderr for 'make dok-tidy'

make it a bit easier to find errors in docbook generated html

tidy doesn't show the filename it's working on, so if
you do a 'make dok-tidy' you get *lots* of output to
stderr but no clue as to which file has all those
errors/warnings