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

> On 6 Nov 2024, at 20:34, David Rowley <dgrowleyml(at)gmail(dot)com> wrote:
>
> On Thu, 7 Nov 2024 at 03:58, Daniel Gustafsson <daniel(at)yesql(dot)se> wrote:
>>
>>> On 6 Nov 2024, at 15:51, Alvaro Herrera <alvherre(at)alvh(dot)no-ip(dot)org> wrote:
>>> 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.
>
> I see in the release notes we're using §. I'm not advocating for any
> particular one, but would it make sense to be consistent on which
> character we use for this?

The § in the release notes is for links leading from the page in question,
whereas the # on the title element is a permalink to the page in question, so I
think it's better to use different symbols given that they perform different
tasks.

--
Daniel Gustafsson