From a2e39659f9dc4ef6f1c40458d0346f7351fc0b3d Mon Sep 17 00:00:00 2001 From: Mac Date: Tue, 28 Jun 2022 13:57:23 -0400 Subject: [PATCH] perf: do not build object files of imports when linking executable --- Lake/Build/Roots.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Lake/Build/Roots.lean b/Lake/Build/Roots.lean index 3e18a0f88b..6d820817cc 100644 --- a/Lake/Build/Roots.lean +++ b/Lake/Build/Roots.lean @@ -83,7 +83,7 @@ def LeanExe.recBuild (self : LeanExe) : IndexT m ActiveFileTarget := do let (_, imports) ← self.root.imports.recBuild let linkTargets := #[Target.active <| ← self.root.o.recBuild] let mut linkTargets ← imports.foldlM (init := linkTargets) fun arr mod => do - return arr.push <| Target.active <| ← mod.o.recBuild + return arr.push <| Target.active <| ← mod.c.recBuild let deps := (← recBuild <| self.pkg.facet &`deps).push self.pkg for dep in deps do for lib in dep.externLibs do linkTargets := linkTargets.push <| Target.active <| ← lib.static.recBuild