Re: Generalising @def*

Gavin Smith <[email protected]> Thu, 2 Feb 2023 21:37:14 +0000

Newsgroups	gmane.comp.tex.texinfo.general
Message-ID	<Y9wtCgYQoCrotF5m@starmint>

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.