diff options
Diffstat (limited to 'CMakeLists.txt')
-rw-r--r-- | CMakeLists.txt | 2 |
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) |