Changing fonts

#1

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]

#2

Theia plugins (VS Code extensions) don’t have access to DOM by design.

#3
#4

VS Code extension allow theming, but we don’t support it yet.

#5

Here is an issue to track it: https://github.com/theia-ide/theia/issues/4831

#6

[levjason]

Thank you.