Zulip Chat Archive
Stream: general
Topic: Highlighting lemma
Patrick Massot (Jul 15 2021 at 11:19):
I noticed since at least yesterday I frequently loose syntax highlighting for the lemma keyword, as in image.png
Gabriel Ebner (Jul 15 2021 at 11:24):
Which vscode-lean version do you have?
Patrick Massot (Jul 15 2021 at 11:26):
Forget about it, I just realized it's my fault. Sorry about the noise.
Last updated: Dec 20 2023 at 11:08 UTC