sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 18:34:06 +00:00
Code Issues Packages Projects Releases Wiki Activity

chore: always use release build for stage 0

Browse Source
This commit is contained in:
Sebastian Ullrich
2020-09-23 14:48:37 +02:00
parent c54d51b0c9
commit c0d40c6f86
1 changed files with 2 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

3
CMakeLists.txt
View File

@@ -17,8 +17,9 @@ ExternalProject_add(stage0
SOURCE_DIR "${LEAN_SOURCE_DIR}/stage0"
SOURCE_SUBDIR src
BINARY_DIR stage0
# always use release build for stage0 since it is assumed to be "good"
# do not rebuild stage0 when git hash changes; it's not from this commit anyway
CMAKE_ARGS -DSTAGE=0 ${CL_ARGS} -DUSE_GITHASH=OFF
CMAKE_ARGS -DSTAGE=0 ${CL_ARGS} -DCMAKE_BUILD_TYPE=Release -DUSE_GITHASH=OFF
BUILD_ALWAYS ON # cmake doesn't auto-detect changes without a download method
INSTALL_COMMAND "" # skip install
)