-
Milian Wolff authored
The navigation widget relies on a crude HTML "parser" which counts "lines". Yes. Only '<br/>' is considered a newline, even though due to line wrapping we can have obviously more lines. Well, without rewriting all of that, also count '</p>' as introducing a new line. This allows us to jump to the 'Show documentation' link then. To make this work reliably, we also fixup the generated HTML to be valid and not nest '<p>' tags. Furthermore, we prevent the ugly line indication marker '<->' being shown when we try to down past the last paragraph.
f633da0d