How to change font size


I must be getting old, I’d like larger fonts. How is that done?


In the meantime you can play with (assuming linux) ~/.zerynth/env/core/official/ide/ide/css/ui-theme/theme-dark.css (or theme-light.css)

Disclaimer: not very good css, but if you just need to increase the editor font size, the first .darkTheme{} is the place to look for


This answer is not up-to-date anymore, is it?
I searched through the css files and randomly changed font-sizes. No effect.
On my screen the font is tiny. Tiny tiny. Piccolissimo.


hi @mcmayer
You can adjust the font size from the menu in the editor. :slight_smile: