Unnamed repository; edit this file 'description' to name the repository.
Fix Lean LSP module imports (#14381)
Co-authored-by: Grégoire Locqueville <[email protected]>
| -rw-r--r-- | book/src/generated/lang-support.md | 2 | ||||
| -rw-r--r-- | 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 aa79bdab..86cc7890 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 da9d1f68..3cfdb8a5 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"] } |