From 5983abcf784d5b00af1fc563b2bdae11463c1cba Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Wed, 13 Sep 2023 17:56:19 -0400
Subject: [PATCH] fix: lake: use manifest opts

specifically, union manifest and config opts (preferring manifest)
---
 src/lake/Lake/Load/Main.lean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/lake/Lake/Load/Main.lean b/src/lake/Lake/Load/Main.lean
index 314e5ffd07..f3c5401e9e 100644
--- a/src/lake/Lake/Load/Main.lean
+++ b/src/lake/Lake/Load/Main.lean
@@ -175,7 +175,9 @@ def Workspace.materializeDeps (ws : Workspace) (manifest : Manifest) (reconfigur
       let depPkgs ← deps.mapM fun dep => fetchOrCreate dep.name do
         if let some entry := pkgEntries.find? dep.name then
           let result ← entry.materialize ws.dir relPkgsDir
-          loadDepPackage ws.dir result pkg.leanOpts dep.opts reconfigure
+          -- Union manifest and configuration options (preferring manifest)
+          let opts := entry.opts.mergeBy (fun _ e _ => e) dep.opts
+          loadDepPackage ws.dir result pkg.leanOpts opts reconfigure
         else if topLevel then
           error <|
             s!"dependency '{dep.name}' not in manifest; " ++