From: Morgan Deters <mdeters@gmail.com>
Date: Mon, 2 May 2011 15:00:42 +0000 (+0000)
Subject: another small fix
X-Git-Tag: cvc5-1.0.0~8566
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8194d145769a87bed07b8ace89eb8b793d14bddd;p=cvc5.git

another small fix
---

diff --git a/src/lib/replacements.h b/src/lib/replacements.h
index 309c8f5b6..a0a9475f4 100644
--- 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'.