From 5ab7ff62b54eecb4ed0d53537e6d9cc584e42c8a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 20 Jan 2015 11:11:35 -0800 Subject: [PATCH] feat(CMakeLists): add --Trust option when building standard/hott libraries --- src/CMakeLists.txt | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index aa020bf266..37a1987e1c 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -372,13 +372,13 @@ if("${CROSS_COMPILE}" MATCHES "ON" OR "${CMAKE_C_COMPILER}" MATCHES "emcc") else() add_custom_target( standard_lib ALL - COMMAND ${PYTHON_EXECUTABLE} ${LEAN_SOURCE_DIR}/../bin/linja all tags + COMMAND ${PYTHON_EXECUTABLE} ${LEAN_SOURCE_DIR}/../bin/linja --Trust all tags 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 + COMMAND ${PYTHON_EXECUTABLE} ${LEAN_SOURCE_DIR}/../bin/linja --Trust all tags DEPENDS ${CMAKE_BINARY_DIR}/shell/lean WORKING_DIRECTORY ${LEAN_SOURCE_DIR}/../hott )