On Thu, Feb 02, 2023 at 07:14:53PM +0000, Gavin Smith wrote: > Yes, we couldn't use @deffn. I am thinking perhaps just @def which > would be like the \defheaderline macro that you've already discovered > in texinfo.tex.
On second thoughts, @def clashes badly with \def in TeX, so there's no way we could add a Texinfo command called @def... @defline or @defheaderline would be ok.
