fix: look here for module as well

leanprover · Nov 21, 2024 · 179e931 · 179e931
1 parent 0f51d9f
commit 179e931
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/ExtractModule.lean b/ExtractModule.lean
@@ -20,6 +20,7 @@ def main : (args : List String) → IO UInt32
       let modName := mod.toName
 
       let sp ← Compat.initSrcSearchPath
+      let sp : SearchPath := (sp : List System.FilePath) ++ [("." : System.FilePath)]
       let fname ← do
         if let some fname ← sp.findModuleWithExt "lean" modName then
           pure fname