max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: minor code cleanup

Browse source
This commit is contained in:
tydeu 2021-08-01 14:08:00 -04:00
parent 293c19d24f
commit 1f51241a8e
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
Lake/BuildTask.lean
View file

@ -44,7 +44,7 @@ def afterTask (task : BuildTask) (act : IO PUnit) : IO BuildTask :=
IO.mapTask (fun x => IO.ofExcept x *> act) task
def afterTaskList (tasks : List BuildTask) (act : IO PUnit) : IO BuildTask :=
IO.mapTasks (fun xs => xs.forM IO.ofExcept *> act) <| tasks
IO.mapTasks (fun xs => xs.forM IO.ofExcept *> act) tasks
instance : HAndThen BuildTask (IO PUnit) (IO BuildTask) :=
⟨afterTask⟩