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

feat: add MTimeBuildTarget -> LeanTarget function

Browse source
This commit is contained in:
tydeu 2021-07-24 08:40:33 -04:00
parent 5770529e09
commit 0d288b9bd3
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
Lake/BuildTarget.lean
View file

@ -118,4 +118,7 @@ def all (targets : List (LeanTarget a)) : IO (LeanTarget PUnit) := do
let task ← BuildTask.all <| targets.map (·.buildTask)
return BuildTarget.mk () ⟨hash, mtime⟩ task
def fromMTimeTarget (target : MTimeBuildTarget a) : LeanTarget a :=
{target with trace := LeanTrace.fromMTime target.mtime}
end LeanTarget