From 29a7d6d05a016024d431d0a3c41dca04bb40a17d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 14 Aug 2014 17:54:42 -0700 Subject: [PATCH] fix(library/hott): remove hott_lib from build, it will be integrated in the standard library Signed-off-by: Leonardo de Moura --- src/CMakeLists.txt | 9 +-------- 1 file changed, 1 insertion(+), 8 deletions(-) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index b4cb8f44b..2a2caf2e4 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -319,16 +319,9 @@ if((${CYGWIN} EQUAL "1") OR (NOT (${CMAKE_SYSTEM_NAME} MATCHES "Windows"))) 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_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 - ) endif() add_custom_target(clean-olean WORKING_DIRECTORY ${LEAN_SOURCE_DIR}/../library - COMMAND find . -type f -name '*.olean' -delete && find . -type f -name '*.d' -delete && find . -type f -name '*.clean' -delete + COMMAND find . -type f -name '*.olean' -delete && find . -type f -name '*.d' -delete && find . -type f -name '*.clean' -delete && find . -type f -name '*.ilean' -delete )