diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-05-19 14:53:27 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-05-19 21:53:27 +0000 |
commit | e2df40dd3b293d5c408f15c7bc99cb8e2d1ebe8a (patch) | |
tree | d30f54b7db3cde2b4fc8f8cafcaa2c93bc17815b /src | |
parent | 081f3676865215c88d057b7d5d832e24e3c263bb (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.
Diffstat (limited to 'src')
-rw-r--r-- | src/options/CMakeLists.txt | 11 |
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 |