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

Syntax

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

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

@ -1,13 +1,18 @@
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" },
dependencies = {
"nvim-lua/plenary.nvim",
},
-- see details below for full configuration options -- see details below for full configuration options
opts = { opts = {