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

[Zoltan Somogyi]

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?

> Should we also add this to the Data-functors section?

Yes, that is a good idea.

Zoltan.