Zulip Chat Archive

Stream: general

Topic: Change VSCode infoview font?


Heather Macbeth (Aug 04 2022 at 20:33):

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 (Aug 04 2022 at 21:01):

Does restarting vscode help?

Patrick Massot (Aug 04 2022 at 21:03):

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

Heather Macbeth (Aug 04 2022 at 21:03):

Gabriel Ebner said:

Does restarting vscode help?

Yes!

Heather Macbeth (Aug 04 2022 at 21:05):

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 (Aug 04 2022 at 21:12):

Yes.


Last updated: Dec 20 2023 at 11:08 UTC