[m-rev.] for post-commit review: ('x')

[Peter Wang]

On Mon, 07 Dec 2020 15:26:57 +1100 "Zoltan Somogyi" <zoltan.somogyi at runbox.com> wrote:
> 
> 
> On Mon, 7 Dec 2020 15:09:06 +1100, Peter Wang <novalazy at gmail.com> wrote:
> > (@code does not add quotes in non-Info output,
> > but both @samp and @code will add quotes in Info output.)
> 
> In that case, should we just delete the @code{} wrappers?

I've replaced @code{} with @t{} which will remove the quotes in Info output,
but retain the monospace font in formats that support it.

> 
> > Should we also add this to the Data-functors section?
> 
> Yes, that is a good idea.

Done.

Peter