mroot/lazyvim
1
0
Fork 0
mirror of https://github.com/LazyVim/LazyVim.git synced 2026-07-25 14:01:06 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Update lean.lua

Browse source
This commit is contained in:
Ben Puryear 2024-07-18 18:57:31 -07:00 • committed by GitHub
parent c317b240ca
commit 70b02135e4
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 6 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
lua/lazyvim/plugins/extras/lang/lean.lua
View file

@ -1,12 +1,10 @@
return { return {
{
recommended = function() recommended = function()
return LazyVim.extras.wants({ return LazyVim.extras.wants({
ft = { "lean" }, ft = { "lean" },
root = { "lean-toolchain" }, root = { "lean-toolchain" },
}) })
end, end,
},
{ {
"Julian/lean.nvim", "Julian/lean.nvim",
event = { "BufReadPre *.lean", "BufNewFile *.lean" }, event = { "BufReadPre *.lean", "BufNewFile *.lean" },