Zulip Chat Archive

Stream: general

Topic: teach VScode new unicode input

Johan Commelin (Jun 11 2018 at 08:04):

How do I teach VScode the fraktur letters?

Gabriel Ebner (Jun 11 2018 at 08:07):

Check out Scott's recent PR on how to add fraktur letters: https://github.com/leanprover/vscode-lean/pull/74/files

Johan Commelin (Jun 11 2018 at 08:13):

Thanks

Last updated: Dec 20 2023 at 11:08 UTC