We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent b02c971 commit 6abaa0cCopy full SHA for 6abaa0c
1 file changed
bins/ExtractSorry.lean
@@ -13,6 +13,7 @@ only have to run them once per project, rather than once per Lean file.
13
-/
14
15
def main (args : List String) : IO Unit := do
16
+ Lean.initSearchPath (← Lean.findSysroot)
17
logRun
18
if let some path := args[0]? then
19
IO.println s!"Running sorry extraction on file {path}."
0 commit comments