Subject: Re: bug#37651: html-name-anchor obsolete, should be html-id-anchor

From: Lars Ingebrigtsen <[email-masked]>
Date: Sun, 03 Nov 2019 16:07:01 +0100

Juri Linkov <[email-masked]> writes:

> A good mnemonic key for HTML id would be C-c C-c #

That's a good mnemonic, so I've now added it (and the <a id...>
skeleton).

-- 
(domestic pets only, the antidote for overdose, milk.)
   bloggy blog: http://lars.ingebrigtsen.no