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

chore: bin_lean should build bin_lean_stage0 first

Browse source
This commit is contained in:
Sebastian Ullrich 2019-12-09 13:06:21 +01:00
parent 185597aef5
commit 1d403dffee
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/shell/CMakeLists.txt
View file

@ -112,10 +112,12 @@ if(NOT STAGE0)
if (MSVC)
ADD_CUSTOM_TARGET(bin_lean ALL
COMMAND "${CMAKE_COMMAND}" -E copy_if_different "$<TARGET_FILE:lean>" "$<TARGET_FILE_DIR:lean>/mpir.dll" "${LEAN_SOURCE_DIR}/../bin/"
DEPENDS bin_lean_stage0
)
else()
ADD_CUSTOM_TARGET(bin_lean ALL
COMMAND "${CMAKE_COMMAND}" -E copy_if_different "$<TARGET_FILE:lean>" "$<TARGET_LINKER_FILE:lean>" "${LEAN_SOURCE_DIR}/../bin/"
DEPENDS bin_lean_stage0
)
ADD_CUSTOM_TARGET(bin_lean_stage2
COMMAND "${CMAKE_COMMAND}" -E copy_if_different "$<TARGET_FILE:lean_stage2>" "${LEAN_SOURCE_DIR}/../bin/"