Zulip Chat Archive
Stream: general
Topic: Red bug
Patrick Massot (Apr 19 2019 at 20:06):
@Gabriel Ebner Is there anything blocking https://github.com/leanprover/vscode-lean/pull/119? I really love the idea of getting rid of those never ending red backgrounds.
Gabriel Ebner (Apr 20 2019 at 11:40):
Just a bit busy at the moment. Should be coming to a vscode near you any second!
Patrick Massot (Apr 20 2019 at 12:24):
Thanks!
Last updated: May 02 2025 at 03:31 UTC