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

chore: disable Lake build

Browse source
This commit is contained in:
Kim Morrison 2024-09-09 20:57:44 +10:00
parent 6aa0c46b04
commit b1a03a471f
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/CMakeLists.txt
View file

@ -620,17 +620,17 @@ else()
endif()
if(NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
add_custom_target(lake_lib ALL
add_custom_target(lake_lib # ALL # TODO restore after stage 0 update
WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
DEPENDS leanshared
COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make Lake
VERBATIM)
add_custom_target(lake_shared ALL
add_custom_target(lake_shared # ALL # TODO restore after stage 0 update
WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
DEPENDS lake_lib
COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make libLake_shared
VERBATIM)
add_custom_target(lake ALL
add_custom_target(lake # ALL # TODO restore after stage 0 update
WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
DEPENDS lake_shared
COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make lake