Skip to content

Commit 322bb1c

Browse files
glocqGrégoire Locqueville
andauthored
Fix Lean LSP module imports (helix-editor#14381)
Co-authored-by: Grégoire Locqueville <gregoire.locqueville@cnrs.fr>
1 parent 34e0f7e commit 322bb1c

2 files changed

Lines changed: 2 additions & 2 deletions

File tree

book/src/generated/lang-support.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -148,7 +148,7 @@
148148
| latex ||| | | | `texlab` |
149149
| ld || || | | |
150150
| ldif || | | | | |
151-
| lean || | | | | `lean` |
151+
| lean || | | | | `lake` |
152152
| ledger || | | | | |
153153
| llvm |||| | | |
154154
| llvm-mir |||| | | |

languages.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -70,7 +70,7 @@ koka = { command = "koka", args = ["--language-server", "--lsstdio"] }
7070
koto-ls = { command = "koto-ls" }
7171
kotlin-lsp = { command = "kotlin-lsp", args = ["--stdio"] }
7272
kotlin-language-server = { command = "kotlin-language-server" }
73-
lean = { command = "lean", args = ["--server"] }
73+
lean = { command = "lake", args = ["serve"] }
7474
ltex-ls = { command = "ltex-ls" }
7575
ltex-ls-plus = { command = "ltex-ls-plus" }
7676
markdoc-ls = { command = "markdoc-ls", args = ["--stdio"] }

0 commit comments

Comments
 (0)