summaryrefslogtreecommitdiff
path: root/test/system
diff options
context:
space:
mode:
authorKshitij Bansal <kshitij@cs.nyu.edu>2014-02-21 10:09:00 -0500
committerKshitij Bansal <kshitij@cs.nyu.edu>2014-02-21 10:09:00 -0500
commitda237313b4c42b5e19e73594c2e909547af782de (patch)
treeb8be9a61cd1905bc664ea692849a4b71f07b1980 /test/system
parent45cd4907560827d1baf822ab3857b1f59efce9f0 (diff)
disable test cvc3_main, attempt to fix dist_check
Diffstat (limited to 'test/system')
-rw-r--r--test/system/Makefile.am4
1 files changed, 2 insertions, 2 deletions
diff --git a/test/system/Makefile.am b/test/system/Makefile.am
index 90867abc9..0306afa68 100644
--- a/test/system/Makefile.am
+++ b/test/system/Makefile.am
@@ -8,8 +8,8 @@ CPLUSPLUS_TESTS = \
statistics
if CVC4_BUILD_LIBCOMPAT
-CPLUSPLUS_TESTS += \
- cvc3_main
+#CPLUSPLUS_TESTS += \
+# cvc3_main
endif
TESTS = $(CPLUSPLUS_TESTS)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback