Add detection for lakefile.toml.

This really only matters if a project has just a lakefile.toml and no lean-toolchain which should basically never happen, but...
Julian · May 17, 2024 · 7219481 · 7219481
1 parent 2828898
commit 7219481
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git a/ftdetect/lean.lua b/ftdetect/lean.lua
@@ -17,7 +17,7 @@ local function detect(filename)
     filetype = 'lean3'
   else
     local find_project_root =
-      require('lspconfig.util').root_pattern('leanpkg.toml', 'lakefile.lean', 'lean-toolchain')
+      require('lspconfig.util').root_pattern('leanpkg.toml', 'lakefile.lean', 'lakefile.toml', 'lean-toolchain')
     local project_root = find_project_root(abspath)
     local succeeded, result
     if project_root then

diff --git a/lua/lean/init.lua b/lua/lean/init.lua
@@ -147,6 +147,7 @@ function lean.current_search_paths()
 
     local executable = (
       vim.loop.fs_stat(root .. '/' .. 'lakefile.lean')
+      or vim.loop.fs_stat(root .. '/' .. 'lakefile.toml')
       or not vim.loop.fs_stat(root .. '/' .. 'leanpkg.toml')
     )
         and 'lake'