#600 no more forgetting to do a make dok-tidy

[Lee]

I'm always forgetting to run tidy on the docs after a 'make dok'.
Can we add tidy to the list of things to do when building the docs?

[Fabian Keil]

I have no objections to this.