projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 6f8200b) | patch
No longer build docs by default. Use make docs. (#7296)
authorGereon Kremer <nafur42@gmail.com>
Mon, 4 Oct 2021 18:05:59 +0000 (11:05 -0700)
committerGitHub <noreply@github.com>
Mon, 4 Oct 2021 18:05:59 +0000 (18:05 +0000)
commit8210ad99ec9ad0a41fd4877878b2d0f20d18304a
tree8fdef4cc1e2cdc16c4ad4442560c3748304d1b25tree
parent6f8200beec0c219d01ce57dab2ad8e3aa283e872commit | 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.
INSTALL.rst diff | blob | history
docs/CMakeLists.txt diff | blob | history
docs/api/cpp/CMakeLists.txt diff | blob | history