From f92d494c4876c7cf86e964f35ffafc855b962aee Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 28 Oct 2021 16:23:14 +0200 Subject: [PATCH] chore: do not distribute Lake examples --- src/CMakeLists.txt | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index e7c549d52f..e6449f80ea 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -522,7 +522,8 @@ install(CODE "execute_process(COMMAND sh -c \"cp ${CMAKE_BINARY_DIR}/lib/*.* \${ install(DIRECTORY "${CMAKE_SOURCE_DIR}" DESTINATION lib/lean FILES_MATCHING PATTERN "*.lean" - PATTERN "*.md") + PATTERN "*.md" + PATTERN examples EXCLUDE) file(COPY ${CMAKE_SOURCE_DIR}/include/lean DESTINATION ${CMAKE_BINARY_DIR}/include FILES_MATCHING PATTERN "*.h")