Re: rethinking @def*

[Gavin Smith]

On Tue, Jul 26, 2022 at 03:24:34PM +0200, Patrice Dumas wrote:
> foobar is not in the 'argument' part of the @deftype*, it is the name.
> It could be bold typewriter, why not, but I think that it is not
> an issue, as there is no inconsistencies nor ill defined semantics.
> We could still change the formatting.

I've made it bold typewriter in the HTML output using CSS.  I've
also compensated for the slightly smaller font size of in monospace
style fonts by specifying font-size: larger.