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"