Hello. I’d like to know the best approach for changing the fonts. I have been able to change the font in the Theia extension with this:
document.documentElement.style.setProperty("–theia-ui-font-family","‘Roboto’, Arial, Sans-serif");
Should the same approach work in a plugin? Thanks.
[original thread by levjason]