Fix Lean LSP module imports (#14381)

Co-authored-by: Grégoire Locqueville <gregoire.locqueville@cnrs.fr>
This commit is contained in:
Grégoire Locqueville
2025-09-10 16:07:59 +02:00
committed by GitHub
parent 34e0f7e82f
commit 322bb1c189
2 changed files with 2 additions and 2 deletions

View File

@@ -148,7 +148,7 @@
| latex | ✓ | ✓ | | | | `texlab` |
| ld | ✓ | | ✓ | | | |
| ldif | ✓ | | | | | |
| lean | ✓ | | | | | `lean` |
| lean | ✓ | | | | | `lake` |
| ledger | ✓ | | | | | |
| llvm | ✓ | ✓ | ✓ | | | |
| llvm-mir | ✓ | ✓ | ✓ | | | |

View File

@@ -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"] }