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

fix(lean): fix typo

Browse source
This commit is contained in:
Zhizhen He 2025-10-09 11:06:02 +08:00 • committed by GitHub
parent a3e52dd346
commit b24b6da930
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 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

@ -108,7 +108,7 @@ return {
priority = 10, priority = 10,
}, },
-- Redirect Lean's stderr messages somehwere (to a buffer by default) -- Redirect Lean's stderr messages somewhere (to a buffer by default)
stderr = { stderr = {
enable = true, enable = true,
-- height of the window -- height of the window