Re: HTML output of @r

[Karl Berry]

    It depends on how @example is implemented. If you used a verbatim-like

I don't see that @example has anything to do with it.  @r is a
general-font-changing command that can and does occur anywhere.