diff options
Diffstat (limited to 'src/include/cvc4_private.h')
| -rw-r--r-- | src/include/cvc4_private.h | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/src/include/cvc4_private.h b/src/include/cvc4_private.h index 3cdb993f1..ccc850787 100644 --- a/src/include/cvc4_private.h +++ b/src/include/cvc4_private.h @@ -20,12 +20,9 @@ #define __CVC4_PRIVATE_H #if ! (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) -# warning A private CVC4 header was included when not building the library or private unit test code. +# error A private CVC4 header was included when not building the library or private unit test code. #endif /* ! (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST) */ -#ifdef __BUILDING_STATISTICS_FOR_EXPORT -# warning A private CVC4 header was included when building a library for export. -#endif /* __BUILDING_STATISTICS_FOR_EXPORT */ #include "cvc4_public.h" #include "cvc4autoconfig.h" |