Unnamed repository; edit this file 'description' to name the repository.
lang: add lakefile.toml to lean.roots (#14678)
| -rw-r--r-- | languages.toml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/languages.toml b/languages.toml index 6a3f36ed..0f867e41 100644 --- a/languages.toml +++ b/languages.toml @@ -1304,7 +1304,7 @@ name = "lean" scope = "source.lean" injection-regex = "lean" file-types = ["lean"] -roots = [ "lakefile.lean" ] +roots = [ "lakefile.lean", "lakefile.toml" ] comment-token = "--" block-comment-tokens = { start = "/-", end = "-/" } language-servers = [ "lean" ] |