diff options
| author | Gereon Kremer <nafur42@gmail.com> | 2021-10-04 11:05:59 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-10-04 18:05:59 +0000 |
| commit | 8210ad99ec9ad0a41fd4877878b2d0f20d18304a (patch) | |
| tree | 8fdef4cc1e2cdc16c4ad4442560c3748304d1b25 | |
| parent | 6f8200beec0c219d01ce57dab2ad8e3aa283e872 (diff) | |
No longer build docs by default. Use make docs. (#7296)
This PR changes our policy when to build the documentation. Beforehand, make docs was included in make and make all.
Now, you need to run make docs explicitly.
| -rw-r--r-- | INSTALL.rst | 7 | ||||
| -rw-r--r-- | docs/CMakeLists.txt | 4 | ||||
| -rw-r--r-- | docs/api/cpp/CMakeLists.txt | 2 |
3 files changed, 5 insertions, 8 deletions
diff --git a/INSTALL.rst b/INSTALL.rst index 95dd063a2..99626a554 100644 --- a/INSTALL.rst +++ b/INSTALL.rst @@ -237,15 +237,12 @@ Building the API documentation of cvc5 requires the following dependencies: `sphinxcontrib-bibtex <https://sphinxcontrib-bibtex.readthedocs.io>`_ - `Breathe <https://breathe.readthedocs.io>`_ -To build the documentation, configure cvc5 with ``./configure.sh --docs``. -Building cvc5 will then include building the API documentation. +To build the documentation, configure cvc5 with ``./configure.sh --docs`` and +run ``make docs`` from within the build directory. The API documentation can then be found at ``<build_dir>/docs/sphinx/index.html``. -To only build the documentation, change to the build directory and call -``make docs``. - To build the documentation for GitHub pages, change to the build directory and call ``make docs-gh``. The content of directory ``<build_dir>/docs/sphinx-gh`` can then be copied over to GitHub pages. diff --git a/docs/CMakeLists.txt b/docs/CMakeLists.txt index c4cc6c283..15c51ed4f 100644 --- a/docs/CMakeLists.txt +++ b/docs/CMakeLists.txt @@ -25,7 +25,7 @@ set(SPHINX_OUTPUT_DIR ${CMAKE_CURRENT_BINARY_DIR}/sphinx) configure_file(conf.py.in ${CMAKE_CURRENT_BINARY_DIR}/conf.py) add_custom_target( - docs ALL + docs DEPENDS docs-cpp docs-java docs-python gen-options COMMAND ${SPHINX_EXECUTABLE} -b html -c ${CMAKE_CURRENT_BINARY_DIR} @@ -46,7 +46,7 @@ add_custom_command( set(SPHINX_GH_OUTPUT_DIR ${CMAKE_CURRENT_BINARY_DIR}/sphinx-gh) add_custom_target( - docs-gh ALL + docs-gh DEPENDS docs # remove existing sphinx-gh/ directory COMMAND ${CMAKE_COMMAND} -E remove_directory ${SPHINX_GH_OUTPUT_DIR} diff --git a/docs/api/cpp/CMakeLists.txt b/docs/api/cpp/CMakeLists.txt index f0b153b57..511dd6e9c 100644 --- a/docs/api/cpp/CMakeLists.txt +++ b/docs/api/cpp/CMakeLists.txt @@ -39,7 +39,7 @@ add_custom_command( ${PROJECT_SOURCE_DIR}/src/api/cpp/cvc5_kind.h COMMENT "Generating doxygen API docs" ) -add_custom_target(docs-cpp ALL DEPENDS ${DOXYGEN_INDEX_FILE}) +add_custom_target(docs-cpp DEPENDS ${DOXYGEN_INDEX_FILE}) # tell parent scope where to find the output xml set(CPP_DOXYGEN_XML_DIR |