Number headers only for documentation
Regarding the numbering of headers introduced in commit 1dd752e6: These are applied to all headlines (in our documentation, auto-generated directory views and the manual). In some places this looks rather ugly, e.g. http://localhost:4444/doc/pldoc/man?section=preddesc.
Could we restrict this formatting to our documentation (directly below /doc)?
Implementation note: our documentation is surrounded with a custom wrapper div (id wiki-wrapper?)