Zulip Chat Archive

Stream: PR reviews

Topic: vscode - add unicode completion to markdown files

Edward Ayers (Oct 17 2018 at 14:20):

https://github.com/leanprover/vscode-lean/pull/96

Last updated: May 02 2025 at 03:31 UTC