diff options
Diffstat (limited to 'src/include/cvc5_private.h')
| -rw-r--r-- | src/include/cvc5_private.h | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/include/cvc5_private.h b/src/include/cvc5_private.h index 1c328ef60..6377997ef 100644 --- a/src/include/cvc5_private.h +++ b/src/include/cvc5_private.h @@ -18,8 +18,8 @@ #define CVC5_PRIVATE_H #if !(defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) -# error A private CVC4 header was included when not building the library or private unit test code. -#endif /* ! (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST) */ +# error A private cvc5 header was included when not building the library or private unit test code. +#endif #include "cvc4autoconfig.h" #include "cvc5_public.h" |