max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: use CMake build type in Lake core build (#10581)

Browse source 
This PR alters the core build Lake configuration file to use the
`CMAKE_BUILD_TYPE` for Lake's `buildType`.
This commit is contained in:
Mac Malone 2025-09-26 23:38:12 -04:00 • committed by GitHub
parent 18832eb600
commit b37d2ce2b9
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/lakefile.toml.in
View file

@ -10,6 +10,9 @@ bootstrap = true
defaultTargets = ["Init", "Std", "Lean", "Lake", "LakeMain", "Leanc"]
# Ensure that Lake and CMake agree on the build type (e.g., `Release`, `Debug`)
buildType = "${CMAKE_BUILD_TYPE}"
# The root of all the compiler output directories
buildDir = "${CMAKE_BINARY_DIR}"