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

On Thu, 18 Jul 2024 at 07:40, David Rowley <dgrowleyml@gmail.com> wrote:
>
> On Thu, 18 Jul 2024 at 17:18, Tom Lane <tgl@sss.pgh.pa.us> wrote:
> > Yeah.  I've found this new feature useful multiple times already,
> > but the '#' icon is as non-mnemonic and unobvious as could possibly
> > be.  OTOH, I don't know of a standard icon for this feature.
>
> I also find it useful and certainly don't want it to disappear.
>

+1. I have also already found it useful.

> There's a unicode character for it.
> https://www.unicodepedia.com/unicode/miscellaneous-symbols-and-pictographs/1f517/link-symbol/
>

+1 for that and a "Link to this heading" tooltip.

Regards,
Dean