michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(build): do not build libraries when cross compiling

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-29 10:00:04 -07:00
parent 1f0171cd57
commit e59889d84f
1 changed files with 9 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/CMakeLists.txt
View file

@ -271,9 +271,12 @@ file(GLOB_RECURSE LEAN_SOURCES
add_style_check_target(style "${LEAN_SOURCES}") add_style_check_target(style "${LEAN_SOURCES}")
add_test(NAME style_check COMMAND ${LEAN_SOURCE_DIR}/cmake/Modules/cpplint.py ${LEAN_SOURCES}) add_test(NAME style_check COMMAND ${LEAN_SOURCE_DIR}/cmake/Modules/cpplint.py ${LEAN_SOURCES})
add_custom_target( if((${CYGWIN} EQUAL "1") OR (NOT (${CMAKE_SYSTEM_NAME} MATCHES "Windows")))
# Only build libraries if we are NOT cross compiling
add_custom_target(
standard_lib ALL standard_lib ALL
COMMAND make LEAN=${CMAKE_BINARY_DIR}/shell/lean COMMAND make LEAN=${CMAKE_BINARY_DIR}/shell/lean
DEPENDS ${CMAKE_BINARY_DIR}/shell/lean DEPENDS ${CMAKE_BINARY_DIR}/shell/lean
WORKING_DIRECTORY ${LEAN_SOURCE_DIR}/../library/standard WORKING_DIRECTORY ${LEAN_SOURCE_DIR}/../library/standard
) )
endif()