OnBotJava font size setting seems to have no effect

[pmichaud]

I don't know when this changed, but the "Font Size" setting in the OnBotJava editor no longer seems to have an effect.

I've tried changing the font size to values as low as 12 and as high as 40 and the font always appears to be the same size on my browser (Google Chrome / Kubuntu Linux).

I know the font size setting worked in previous versions of OnBotJava. Being able to set a large font size is important whenever I'm trying to teach/present OnBotJava programming in classroom or online workshop environments (e.g. for projection).

Thanks,

Pm