diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2018-09-26 18:28:15 -0700 |
---|---|---|
committer | Aina Niemetz <aina.niemetz@gmail.com> | 2018-09-26 18:28:15 -0700 |
commit | cb5ac59af1836486b8ccfdb1c44390de9a8c80d8 (patch) | |
tree | f90d14dd6eebe9ab70ab79a2c6966280747d6f84 /cmake/ConfigDebug.cmake | |
parent | 672d1347c2daeddb8c434ea996f95ba555d22589 (diff) |
cmake: Only print dumping warning if not disabled by user. (#2543)
Diffstat (limited to 'cmake/ConfigDebug.cmake')
-rw-r--r-- | cmake/ConfigDebug.cmake | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/cmake/ConfigDebug.cmake b/cmake/ConfigDebug.cmake index 9c9f5ec10..a4331bfce 100644 --- a/cmake/ConfigDebug.cmake +++ b/cmake/ConfigDebug.cmake @@ -19,9 +19,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() |