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

chore: update stage0

Browse source
This commit is contained in:
Markus Himmel 2024-08-07 17:45:45 +02:00 • committed by Sebastian Ullrich
parent 3b14642c42
commit 63c4de5fea
1 changed files with 7 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
stage0/src/CMakeLists.txt generated
View file

@ -579,13 +579,13 @@ else()
string(APPEND CMAKE_EXE_LINKER_FLAGS " -lInit_shared -lleanshared")
endif()
#if(NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
# add_custom_target(lake ALL
# WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
# DEPENDS leanshared
# COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make Lake
# VERBATIM)
#endif()
if(NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
add_custom_target(lake ALL
WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
DEPENDS leanshared
COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make Lake
VERBATIM)
endif()
if(PREV_STAGE)
add_custom_target(update-stage0