another small fix

diff --git a/src/lib/replacements.h b/src/lib/replacements.h
index 309c8f5b6dace2e5a9ab264d819f644b143c643a..a0a9475f48d0589ab4e0d3a035c355b5c52f7c2d 100644 (file)
--- a/src/lib/replacements.h
+++ b/src/lib/replacements.h
@@ -27,7 +27,7 @@
 #  if defined(__BUILDING_CVC4PARSERLIB) || defined(__BUILDING_CVC4PARSERLIB_UNIT_TEST)
 #    include "cvc4parser_private.h"
 #  else
-#    if defined(__BUILDING_CVC4DRIVER __BUILDING_CVC4_SYSTEM_TEST)
+#    if defined(__BUILDING_CVC4DRIVER) || defined(__BUILDING_CVC4_SYSTEM_TEST)
 #      include "cvc4autoconfig.h"
 #    else
 #      error Must be building libcvc4 or libcvc4parser to use replacement functions.  This is because replacement function headers should never be publicly-depended upon, as they should not be installed on user machines with 'make install'.