bug#12973: @: overused in manual

[Eli Zaretskii]

> Date: Fri, 23 Nov 2012 12:50:34 -0800
> From: Paul Eggert <eggert@cs.ucla.edu>
> CC: 12973@debbugs.gnu.org
> 
> On 11/23/2012 11:46 AM, Eli Zaretskii wrote:
> > Why do you say it has no effect in this case?
> 
> It has no effect in TeX because TeX already does
> the right thing with initials.  TeX assumes that
> "." ends a sentence unless it's preceded by a capital
> letter.  "Jay K. Adams" has a capital letter before
> the period so no @: is needed after the period.

This ought to be in the Texinfo manual, then.  I suggest to report
this to Texinfo maintainers, because the latest manual doesn't mention
that.