[Users] adjusting font size displayed by the "fancy" plugin

[»Q«]

On Mon, 6 Jun 2016 14:06:53 -0700
Lyle Bickley <lbickley at bickleywest.com> wrote:

> I have tried unsuccessfully to create several CSS stylesheets to
> correct the default "fancy" plugin font size of 6 or 8 points. None of
> my stylesheets had any effect on font size - including one which
> adjusts the size of font depending on the size of the screen. All
> were copied from known running sources.
> 
> Does someone have stylesheets that are known to work with this plugin?

This works for me:

* { font-family : "Dejavu Mono", Monospace; font-size : 13pt }

I've got some other stuff in the css file, but that's the only rule
that handles font size.