summaryrefslogtreecommitdiff
path: root/src/include
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2018-09-04 14:59:19 -0700
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>2018-09-04 16:59:19 -0500
commit747a9a248da073911e1c0da34c38f0648421a087 (patch)
tree98449a71c66d0ad427b8c8dc6f0ed1b9fbccdfbe /src/include
parent29bf7d6a937ab50c4dd92a30d7beb36a4001ead6 (diff)
Remove CVC3 compatibility layer (#2418)
Diffstat (limited to 'src/include')
-rw-r--r--src/include/cvc4_private_library.h2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/include/cvc4_private_library.h b/src/include/cvc4_private_library.h
index 6fa4410f8..92ed555fd 100644
--- a/src/include/cvc4_private_library.h
+++ b/src/include/cvc4_private_library.h
@@ -19,7 +19,7 @@
#ifndef __CVC4_PRIVATE_LIBRARY_H
#define __CVC4_PRIVATE_LIBRARY_H
-#if ! (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST) || defined(__BUILDING_CVC4PARSERLIB) || defined(__BUILDING_CVC4PARSERLIB_UNIT_TEST) || defined(__BUILDING_CVC4COMPATLIB) || defined(__BUILDING_CVC4DRIVER))
+#if ! (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST) || defined(__BUILDING_CVC4PARSERLIB) || defined(__BUILDING_CVC4PARSERLIB_UNIT_TEST) || defined(__BUILDING_CVC4DRIVER))
# error A "private library" CVC4 header was included when not building the library, driver, or private unit test code.
#endif /* ! (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST || __BUILDING_CVC4PARSERLIB || __BUILDING_CVC4PARSERLIB_UNIT_TEST || __BUILDING_CVC4DRIVER) */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback