projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b016f60) | patch
Move docs upload to a different workflow (#6512)
authorGereon Kremer <nafur42@gmail.com>
Wed, 12 May 2021 17:13:06 +0000 (19:13 +0200)
committerGitHub <noreply@github.com>
Wed, 12 May 2021 17:13:06 +0000 (17:13 +0000)
commit62e1f3ffd0688bc229130a1964c3e50b4575e48f
tree3fd42c8281fc60d28714877c5df0a7f4e9502d85tree
parentb016f603f2a3709faaf90008a09f2567d7283ff3commit | diff
Move docs upload to a different workflow (#6512)

This PR (finally, I hope) uses a proper setup for uploading the documentation. One of the CI jobs generates the documentation and stores it in an artifact. Another workflow is triggered (via workflow_run) and then uploads this artifact. Only this setup seems to properly work for PR builds.
.github/workflows/ci.yml diff | blob | history
.github/workflows/docs_cleanup.yml diff | blob | history
.github/workflows/docs_upload.yml [new file with mode: 0644] blob