From 322bb1c189af1ec29be449058c1116378bcf10e1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Gr=C3=A9goire=20Locqueville?= Date: Wed, 10 Sep 2025 16:07:59 +0200 Subject: [PATCH] Fix Lean LSP module imports (#14381) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Grégoire Locqueville --- book/src/generated/lang-support.md | 2 +- languages.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/book/src/generated/lang-support.md b/book/src/generated/lang-support.md index aa79bdaba..86cc78901 100644 --- a/book/src/generated/lang-support.md +++ b/book/src/generated/lang-support.md @@ -148,7 +148,7 @@ | latex | ✓ | ✓ | | | | `texlab` | | ld | ✓ | | ✓ | | | | | ldif | ✓ | | | | | | -| lean | ✓ | | | | | `lean` | +| lean | ✓ | | | | | `lake` | | ledger | ✓ | | | | | | | llvm | ✓ | ✓ | ✓ | | | | | llvm-mir | ✓ | ✓ | ✓ | | | | diff --git a/languages.toml b/languages.toml index da9d1f681..3cfdb8a5a 100644 --- a/languages.toml +++ b/languages.toml @@ -70,7 +70,7 @@ koka = { command = "koka", args = ["--language-server", "--lsstdio"] } koto-ls = { command = "koto-ls" } kotlin-lsp = { command = "kotlin-lsp", args = ["--stdio"] } kotlin-language-server = { command = "kotlin-language-server" } -lean = { command = "lean", args = ["--server"] } +lean = { command = "lake", args = ["serve"] } ltex-ls = { command = "ltex-ls" } ltex-ls-plus = { command = "ltex-ls-plus" } markdoc-ls = { command = "markdoc-ls", args = ["--stdio"] }