Re: rethinking @def*

[Gavin Smith]

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