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

chore: apply required change after update-stage0

Browse source 
cc @Kha
This commit is contained in:
Leonardo de Moura 2019-11-20 08:00:11 -08:00
parent dbb7a0bfff
commit 49f1f0dfe3
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/shell/CMakeLists.txt
View file

@ -14,7 +14,7 @@ if(NOT STAGE0)
# '-G Ninja' complains otherwise
BYPRODUCTS "${CMAKE_BINARY_DIR}/stage1/libleanstdlib.a"
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../library"
COMMAND ${CMAKE_COMMAND} -E env "LEAN_PATH=." $(MAKE) "${CMAKE_BINARY_DIR}/stage1/libleanstdlib.a" "LEAN=$<TARGET_FILE:lean_stage0>" "LEANC_OPTS=${LEANC_OPTS}" "STAGE1_OUT=${CMAKE_BINARY_DIR}/stage1"
COMMAND ${CMAKE_COMMAND} -E env "LEAN_PATH=Init=Init" $(MAKE) "${CMAKE_BINARY_DIR}/stage1/libleanstdlib.a" "LEAN=$<TARGET_FILE:lean_stage0>" "LEANC_OPTS=${LEANC_OPTS}" "STAGE1_OUT=${CMAKE_BINARY_DIR}/stage1"
DEPENDS stage0)
set_target_properties(leanstdlib PROPERTIES
IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/stage1/libleanstdlib.a"