Skip to content

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?)