Re: using @titleplage in every format

[Patrice Dumas]

On Tue, Feb 19, 2019 at 05:52:23PM +0200, Eli Zaretskii wrote:
> > Date: Tue, 19 Feb 2019 01:27:23 +0100
> > From: Patrice Dumas <address@hidden>
> > Cc: address@hidden
> > 
> > > Checking Texinfo's own manual, @top has an argument and is used as
> > > "@top Texinfo".  I haven't checked but I suspect TeX would output a 
> > > large heading from this.
> > 
> > Indeed, but I propose to leave @top without argument, like
> > @top
> 
> FWIW, I don't think we should make such backward-incompatible changes
> in such veteran commands.

I am not saying that @top should ignore its argument, what I am saying
is that we should propose to users to leave @top without argument when
there is already a @titlepage in the documentation.

-- 
Pat