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

> On 18 Nov 2024, at 20:51, Bruce Momjian <bruce(at)momjian(dot)us> wrote:
>
> On Wed, Nov 6, 2024 at 03:58:18PM +0100, Daniel Gustafsson wrote:
>>> On 6 Nov 2024, at 15:51, Alvaro Herrera <alvherre(at)alvh(dot)no-ip(dot)org> wrote:
>>>
>>> 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?
>>
>> You're right, I mistakenly remembered there being no concensus and didn't
>> re-read the thread when it was revived with the patch in question. Re-reading
>> it now I see multiple +1's for using a ¶ instead so will fix that. Thanks for
>> the heads-up.
>
> Uh, has this change been made? I still see "#":

It hasn't been changed, I was hoping to hear more opinions but since there has
been none I will go ahead with the result of the previous discussion which
landed in ¶.

Hearing no complaints against the fix for the issue Álvaro identified I'll push
that as well.

--
Daniel Gustafsson