From 0d288b9bd33903271ec4b5123b482ceea711e3ea Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Sat, 24 Jul 2021 08:40:33 -0400
Subject: [PATCH] feat: add `MTimeBuildTarget` -> `LeanTarget` function

---
 Lake/BuildTarget.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/Lake/BuildTarget.lean b/Lake/BuildTarget.lean
index 6becb2cc70..c62d8d6802 100644
--- a/Lake/BuildTarget.lean
+++ b/Lake/BuildTarget.lean
@@ -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