From f8eba36b0a341e077eac9590132c21ae995efc4f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 29 Jul 2014 10:06:39 -0700 Subject: [PATCH] fix(build): set LEAN_PATH before make standard and hott libraries Signed-off-by: Leonardo de Moura --- src/CMakeLists.txt | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 2b624fc11..97f6dc359 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -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 )