Skip to content

Commit

Permalink
chore: quick touch-up
Browse files Browse the repository at this point in the history
  • Loading branch information
tydeu committed May 10, 2024
1 parent bbf43af commit 747bc3e
Showing 1 changed file with 0 additions and 1 deletion.
1 change: 0 additions & 1 deletion src/lake/Lake/Build/Actions.lean
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,6 @@ def compileLeanModule
for dynlib in dynlibs do
args := args.push s!"--load-dynlib={dynlib}"
args := args.push "--json"
show LogIO _ from do
withLogErrorPos do
let out ← rawProc {
args
Expand Down

0 comments on commit 747bc3e

Please sign in to comment.