summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2021-05-19 14:53:27 -0700
committerGitHub <noreply@github.com>2021-05-19 21:53:27 +0000
commite2df40dd3b293d5c408f15c7bc99cb8e2d1ebe8a (patch)
treed30f54b7db3cde2b4fc8f8cafcaa2c93bc17815b
parent081f3676865215c88d057b7d5d832e24e3c263bb (diff)
Make output list of `mkoptions.py` more accurate (#6572)
After commit 6dc5b74, cvc5 was always being almost completely rebuilt, even if there hadn't been any changes if cvc5 was configured not to produce documentation (the default). This was because mkoptions.py only produces the options_generated.rst file when documentation is enabled. However, it was unconditionally declared to be an output of the script in CMakeLists.txt. As a result, the options (and thus most of the code base) were rebuilt every time because the file was missing in builds without documentation. This commit modifies the output list depending on the configuration.
-rw-r--r--src/options/CMakeLists.txt11
1 files changed, 10 insertions, 1 deletions
diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt
index 997c6850a..2107865c0 100644
--- a/src/options/CMakeLists.txt
+++ b/src/options/CMakeLists.txt
@@ -70,11 +70,20 @@ libcvc5_add_sources(GENERATED options.h options.cpp ${options_gen_cpp_files})
list_prepend(options_toml_files "${CMAKE_CURRENT_LIST_DIR}/" abs_toml_files)
+set(options_gen_doc_files "")
+if (BUILD_DOCS)
+ list(
+ APPEND
+ options_gen_doc_files
+ "${CMAKE_BINARY_DIR}/docs/options_generated.rst"
+ )
+endif()
+
add_custom_command(
OUTPUT
options.h options.cpp
${options_gen_cpp_files} ${options_gen_h_files}
- ${CMAKE_BINARY_DIR}/docs/options_generated.rst
+ ${options_gen_doc_files}
COMMAND
${PYTHON_EXECUTABLE}
${CMAKE_CURRENT_LIST_DIR}/mkoptions.py
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback