doc: Make HTML ids discoverable
authorPeter Eisentraut <[email protected]>
Thu, 13 Apr 2023 08:15:20 +0000 (10:15 +0200)
committerPeter Eisentraut <[email protected]>
Thu, 13 Apr 2023 08:16:33 +0000 (10:16 +0200)
commite2922702a3027945f139f9b0c7b4686423304e21
tree1b1a96497a7c92b780df1c02ce97be4ecb595789
parenta34901dd03edb473ddbd81ee5c7332575f6d8881
doc: Make HTML ids discoverable

In the HTML output, this decorates section headers and variable list
terms with a marker ("#") that is a link to the same section/term.
That way, links inside a page can be discovered for easier sharing.
The marker only appears when hovering.

This now requires that all elements that are candidates for such a
link have an id attribute.  Otherwise, an error will be generated.
All previously missing ids have been added prior to this patch.

Author: Brar Piening <[email protected]>
Reviewed-by: Karl O. Pinc <[email protected]>
Discussion: https://www.postgresql.org/message-id/flat/CAB8KJ=jpuQU9QJe4+RgWENrK5g9jhoysMw2nvTN_esoOU0=a_w@mail.gmail.com
doc/src/sgml/stylesheet-html-common.xsl
doc/src/sgml/stylesheet.css