Typo in Texinfo manual

[Arni Magnusson]

There's a small typo in the Texinfo manual, where texinfo.txi says:

  @code{@@deffn} and prints

It should probably say:

  @code{@@deffn} prints

Cheers,

Arni