Skip to content

Commit

Permalink
fix: use user's Lean search path in linter (#980)
Browse files Browse the repository at this point in the history
  • Loading branch information
tydeu authored Oct 4, 2024
1 parent 63c1c38 commit 13f9b00
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion scripts/runLinter.lean
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ unsafe def main (args : List String) : IO Unit := do
| name => some name
| _ => none
| IO.eprintln "Usage: runLinter [--update] [Batteries.Data.Nat.Basic]" *> IO.Process.exit 1
searchPathRef.set compile_time_search_path%
initSearchPath (← findSysroot)
let mFile ← findOLean module
unless (← mFile.pathExists) do
-- run `lake build module` (and ignore result) if the file hasn't been built yet
Expand Down

0 comments on commit 13f9b00

Please sign in to comment.