lean.nvim icon indicating copy to clipboard operation
lean.nvim copied to clipboard

Published 20 hours ago • verified publisher icon Julian

(Re-)review / harmonize with the VSCode options

Open Julian opened this issue 6 months ago • 0 comments

Particularly ones from https://github.com/leanprover/vscode-lean4/pull/302/files

Julian avatar Jan 03 '24 18:01 Julian