From ddbba944d42a1479ec9e4f350b9a270b008c01f0 Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Tue, 24 Jun 2025 07:39:29 -0400 Subject: [PATCH] fix: pass Lean CMake CI options to the Lake build (#8823) This PR passes Lean options configured via CMake variables onto the Lake build. For example, this will ensure CI' setting of `warningAsError` via `LEAN_EXTRA_MAKE_OPTS` reaches Lake. --- src/lakefile.toml.in | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/lakefile.toml.in b/src/lakefile.toml.in index 640b5ccbee..eda69ea848 100644 --- a/src/lakefile.toml.in +++ b/src/lakefile.toml.in @@ -25,6 +25,10 @@ leanLibDir = "lib/lean" # Destination for static libraries nativeLibDir = "lib/lean" +# Additional options derived from the CMake configuration +# For example, CI will set `-DwarningAsError=true` through this +moreLeanArgs = [${LEAN_EXTRA_OPTS_TOML}] + [[lean_lib]] name = "Init" libName = "${LAKE_LIB_PREFIX}Init"