From cb5ac59af1836486b8ccfdb1c44390de9a8c80d8 Mon Sep 17 00:00:00 2001
From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Wed, 26 Sep 2018 18:28:15 -0700
Subject: cmake: Only print dumping warning if not disabled by user. (#2543)

---
 cmake/ConfigTesting.cmake | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'cmake/ConfigTesting.cmake')

diff --git a/cmake/ConfigTesting.cmake b/cmake/ConfigTesting.cmake
index 3c995e421..7feaf5129 100644
--- a/cmake/ConfigTesting.cmake
+++ b/cmake/ConfigTesting.cmake
@@ -16,9 +16,8 @@ cvc4_set_option(ENABLE_PROOFS ON)
 cvc4_set_option(ENABLE_TRACING ON)
 # enable_dumping=yes
 if(ENABLE_PORTFOLIO)
-  if(ENABLE_DUMPING)
-    message(FATAL_ERROR "Dumping not supported with a portfolio build.")
-  else()
+  # Only print warning if dumping was not explicitely disabled by the user.
+  if(${ENABLE_DUMPING} STREQUAL "IGNORE")
     message(WARNING
       "Disabling dumping support, not supported with a portfolio build.")
   endif()
-- 
cgit v1.2.3