From b33aa09384e638ce09a84110bc95cb2ca3fcbfc9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 8 Jul 2022 16:40:51 -0700 Subject: [PATCH] chore: the `for in` elaborator now propagates the element type to the body --- Lake/Build/Module.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Lake/Build/Module.lean b/Lake/Build/Module.lean index f51964ac34..34a2925bf5 100644 --- a/Lake/Build/Module.lean +++ b/Lake/Build/Module.lean @@ -71,7 +71,7 @@ variable [Monad m] [MonadBuildStore m] def recBuildExternalDynlibs (pkgs : Array Package) [MonadLog m] : IndexT m (Array ActiveFileTarget × Array FilePath) := do let mut libDirs := #[] - let mut targets := #[] + let mut targets : Array ActiveFileTarget := #[] for pkg in pkgs do libDirs := libDirs.push pkg.libDir let externLibTargets ← pkg.externLibs.mapM (·.shared.recBuild)