diff options
author | Gereon Kremer <nafur42@gmail.com> | 2021-05-08 01:14:13 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-05-07 16:14:13 -0700 |
commit | a10b52cd8b9746168e167de94094227ebebe4180 (patch) | |
tree | 0a7becfc58abca1500a95fc8d884dbdea8bcfde5 /src/util/index.h | |
parent | bf62473ea3bed27f13f0eb320cea404ebadb490e (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.
Diffstat (limited to 'src/util/index.h')
0 files changed, 0 insertions, 0 deletions