summaryrefslogtreecommitdiff
path: root/CMakeLists.txt
diff options
context:
space:
mode:
Diffstat (limited to 'CMakeLists.txt')
-rw-r--r--CMakeLists.txt2
1 files changed, 1 insertions, 1 deletions
diff --git a/CMakeLists.txt b/CMakeLists.txt
index 862fc2ae5..23a52db59 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -433,7 +433,7 @@ if(ENABLE_PROOFS)
endif()
add_subdirectory(doc)
-add_subdirectory(examples)
+add_subdirectory(examples EXCLUDE_FROM_ALL)
add_subdirectory(src)
add_subdirectory(test)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback