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

fix(build): set LEAN_PATH before make standard and hott libraries

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

4
src/CMakeLists.txt
View file

@ -312,14 +312,14 @@ 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=${CMAKE_BINARY_DIR}/shell/lean
COMMAND make -j ${PROCESSOR_COUNT} LEAN_PATH=.:${LEAN_SOURCE_DIR}/../library/standard LEAN=${CMAKE_BINARY_DIR}/shell/lean
DEPENDS ${CMAKE_BINARY_DIR}/shell/lean
WORKING_DIRECTORY ${LEAN_SOURCE_DIR}/../library/standard
)
add_custom_target(
hott_lib ALL
COMMAND make -j ${PROCESSOR_COUNT} LEAN="${CMAKE_BINARY_DIR}/shell/lean" LEAN_OPTIONS="--hott"
COMMAND make -j ${PROCESSOR_COUNT} LEAN_PATH=.:${LEAN_SOURCE_DIR}/../library/hott LEAN="${CMAKE_BINARY_DIR}/shell/lean" LEAN_OPTIONS="--hott"
DEPENDS ${CMAKE_BINARY_DIR}/shell/lean
WORKING_DIRECTORY ${LEAN_SOURCE_DIR}/../library/hott
)