Re: A minor bug in doc. Hovering over heading shows # besides it.

On 2024-Nov-06, Daniel Gustafsson wrote:

> Committed, and with some help from Magnus, the docs site has been reloaded with
> the new CSS.  Everything seems to behave as expected when testing in Firefox,
> Safari, Chrome and Edge.

Ah, but we kept the #?  I thought it was going to be changed to ¶ ...
was there any voice against that?

-- 
Álvaro Herrera               48°01'N 7°57'E  —  https://www.EnterpriseDB.com/