diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 17c7bd3509..4982f39e79 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -855,6 +855,12 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Windows") set(LAKE_LIB_PREFIX "lib") endif() +if(${CMAKE_BUILD_TYPE} MATCHES "Debug|Release|RelWithDebInfo|MinSizeRel") + set(CMAKE_BUILD_TYPE_TOML "${CMAKE_BUILD_TYPE}") +else() + set(CMAKE_BUILD_TYPE_TOML "Release") +endif() + if(USE_LAKE) configure_file(${LEAN_SOURCE_DIR}/lakefile.toml.in ${CMAKE_BINARY_DIR}/lakefile.toml) # copy for editing diff --git a/src/lakefile.toml.in b/src/lakefile.toml.in index 7c557d1e24..28eb6c6892 100644 --- a/src/lakefile.toml.in +++ b/src/lakefile.toml.in @@ -10,8 +10,8 @@ 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}" +# Have Lake use CMake's build type (e.g., `Release`, `Debug`) where possible +buildType = "${CMAKE_BUILD_TYPE_TOML}" # The root of all the compiler output directories buildDir = "${CMAKE_BINARY_DIR}"