Change VSCode infoview font?

Stream: general

[Heather Macbeth]

For a talk, I'd like to change the font in the infoview. Is this possible? When I edit the VSCode "Editor: Font Family" setting, it changes the font in the main Lean file, but not in the infoview.

[Gabriel Ebner]

Does restarting vscode help?

[Patrick Massot]

You can also tweak widgets as I explained to Yaël a couple of days ago. This allows many things.

[Heather Macbeth]

Gabriel Ebner said:

Does restarting vscode help?

Yes!

[Heather Macbeth]

Patrick Massot said:

You can also tweak widgets as I explained to Yaël a couple of days ago. This allows many things.

This sounds potentially useful, thanks. You mean this conversation right?

[Patrick Massot]

Yes.