#23 Make the style sheet (css) editable (user pref)

[Anonymous]

I would like to be able to set the fonts and their sizes for the different
styles. Currently, the code style uses too small a font when compared to
the normal text. So, if I click on 'bigger text', the normal text is much too
big when I make the source code legible.

Also, source code uses a double line height, which I would to see reduced
to a single one.