projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: dc84ee8) | patch
Fix a couple of issues with uploading docs for releases (#7543)
authorGereon Kremer <nafur42@gmail.com>
Mon, 1 Nov 2021 20:09:41 +0000 (13:09 -0700)
committerGitHub <noreply@github.com>
Mon, 1 Nov 2021 20:09:41 +0000 (20:09 +0000)
commite93fd13d1bebc1ca916033c481f3e4864a0dea11
treefda68319fc7645bd5593c224302bfe50b8e387c9tree
parentdc84ee87902f089522336a0c63435b22b143856fcommit | diff
Fix a couple of issues with uploading docs for releases (#7543)

This PR fixes multiple issues with uploading docs for releases: the regular upload moved the generated docs, so the release upload would not find the docs; the check whether we have a release was incorrect; we probably want $NAME instead of docs-$NAME here.
.github/workflows/docs_upload.yml diff | blob | history