On Sun, Jul 31, 2022 at 09:23:54PM +0100, Gavin Smith wrote: > As you noted, the name is in a typewriter font due to <code> rather than > <strong> being used. Maybe we discussed this already, but I think we > should reconsider this change.
I think this change is probably a good idea as it makes it consistent with TeX. We should make sure that the definition name is accessible with CSS. Earlier, we recommended using a "dt strong" CSS selector. https://lists.gnu.org/archive/html/bug-texinfo/2020-11/msg00041.html
