From 0034ad9b34bafe973e062e391bca9ccda10d4885 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 5 Dec 2014 14:38:45 -0800 Subject: [PATCH] feat(build): add HoTT library to build --- bin/linja | 2 +- src/CMakeLists.txt | 6 ++++++ 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/bin/linja b/bin/linja index 67f9a7c26a..920a5453ef 100755 --- a/bin/linja +++ b/bin/linja @@ -506,7 +506,7 @@ def find_lean_files(args): files -= set(find_files(project_dir, pattern)) has_lean = False has_hlean = False - for file in args.targets: + for file in files: if file.endswith(".lean"): has_lean = True if file.endswith(".hlean"): diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 39dee9b6b4..690a768e2e 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -373,6 +373,12 @@ else() DEPENDS ${CMAKE_BINARY_DIR}/shell/lean WORKING_DIRECTORY ${LEAN_SOURCE_DIR}/../library ) + add_custom_target( + hott_lib ALL + COMMAND ${PYTHON_EXECUTABLE} ${LEAN_SOURCE_DIR}/../bin/linja all tags + DEPENDS ${CMAKE_BINARY_DIR}/shell/lean + WORKING_DIRECTORY ${LEAN_SOURCE_DIR}/../hott + ) endif() add_custom_target(clean-olean