From 179e931b437d7b564ddf44d68b60e143c18940c4 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Thu, 21 Nov 2024 16:36:14 +0100 Subject: [PATCH] fix: look here for module as well --- ExtractModule.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/ExtractModule.lean b/ExtractModule.lean index 034e91c..2d4d6de 100644 --- 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