summaryrefslogtreecommitdiff
path: root/test/system
diff options
context:
space:
mode:
authorAina Niemetz <aina.niemetz@gmail.com>2018-09-14 14:21:35 -0700
committerMathias Preiner <mathias.preiner@gmail.com>2018-09-22 16:30:59 -0700
commit0a41a21cedc789262f3035aa91ff6b924f309b4e (patch)
treeeae28a622352c818e043b0ac3adba60c3e14a0c3 /test/system
parent15a7249a2aa33187e766d6f828a503e5c937b9cf (diff)
cmake: Do not build examples and unit and system tests by default.
Diffstat (limited to 'test/system')
-rw-r--r--test/system/CMakeLists.txt3
1 files changed, 2 insertions, 1 deletions
diff --git a/test/system/CMakeLists.txt b/test/system/CMakeLists.txt
index 01b4a384d..2ca33d1e9 100644
--- a/test/system/CMakeLists.txt
+++ b/test/system/CMakeLists.txt
@@ -8,7 +8,8 @@ include_directories(${CMAKE_BINARY_DIR}/src)
# > system tests
add_custom_target(systemtests
- COMMAND ctest --output-on-failure -L "system" -j${NTHREADS} $(ARGS))
+ COMMAND ctest --output-on-failure -L "system" -j${NTHREADS} $(ARGS)
+ DEPENDS cvc4)
set(CVC4_SYSTEM_TEST_FLAGS
-D__BUILDING_CVC4_SYSTEM_TEST -D__STDC_LIMIT_MACROS -D__STDC_FORMAT_MACROS)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback