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