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

fix(CMakeLists.txt): use bin/lean to build library

Browse source 
close #49
This commit is contained in:
Soonho Kong 2014-08-14 18:11:38 -07:00
parent b18124e1a2
commit 74b665ea06
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/CMakeLists.txt
View file

@ -315,7 +315,7 @@ 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
COMMAND make -j ${PROCESSOR_COUNT} LEAN_PATH=.:${LEAN_SOURCE_DIR}/../library/standard LEAN=${CMAKE_BINARY_DIR}/shell/lean
COMMAND make -j ${PROCESSOR_COUNT} LEAN_PATH=.:${LEAN_SOURCE_DIR}/../library/standard LEAN="${CMAKE_SOURCE_DIR}/../bin/lean"
DEPENDS ${CMAKE_BINARY_DIR}/shell/lean
WORKING_DIRECTORY ${LEAN_SOURCE_DIR}/../library/standard
)