projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: bf62473) | patch
Integrate documentation build with the regular CI workflow (#6490)
authorGereon Kremer <nafur42@gmail.com>
Fri, 7 May 2021 23:14:13 +0000 (01:14 +0200)
committerGitHub <noreply@github.com>
Fri, 7 May 2021 23:14:13 +0000 (16:14 -0700)
commita10b52cd8b9746168e167de94094227ebebe4180
tree0a7becfc58abca1500a95fc8d884dbdea8bcfde5tree
parentbf62473ea3bed27f13f0eb320cea404ebadb490ecommit | diff
Integrate documentation build with the regular CI workflow (#6490)

The new documentation workflow requires building CVC5 again in a separate workflow, which takes quite some time.
This PR integrates building the documentation with the regular CI workflow.
.github/workflows/ci.yml diff | blob | history
.github/workflows/docs_update.yml [deleted file] blob | history