We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent a18223f commit 1d63ab0Copy full SHA for 1d63ab0
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