max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: recurse in findAllWithExt

Browse source
This commit is contained in:
Sebastian Ullrich 2022-01-14 18:59:58 +01:00
parent 6ec406b7d0
commit 753e396705
1 changed files with 1 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Util/Path.lean
View file

@ -41,9 +41,7 @@ def findAllWithExt (sp : SearchPath) (ext : String) : IO (Array FilePath) := do
let mut paths := #[]
for p in sp do
if (← p.isDir) then
for e in (← p.readDir) do
if e.fileName.endsWith s!".{ext}" then
paths := paths.push e.path
paths := paths ++ (← p.walkDir).filter (·.extension == some ext)
paths
end SearchPath