How to change font size


#1

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


#2



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



#3

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.


#4

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