diff options
| author | Gereon Kremer <nafur42@gmail.com> | 2021-11-01 13:09:41 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-11-01 20:09:41 +0000 |
| commit | e93fd13d1bebc1ca916033c481f3e4864a0dea11 (patch) | |
| tree | fda68319fc7645bd5593c224302bfe50b8e387c9 /.github/workflows/docs_upload.yml | |
| parent | dc84ee87902f089522336a0c63435b22b143856f (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.
Diffstat (limited to '.github/workflows/docs_upload.yml')
| -rw-r--r-- | .github/workflows/docs_upload.yml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/.github/workflows/docs_upload.yml b/.github/workflows/docs_upload.yml index 9aadd6647..fd489beee 100644 --- a/.github/workflows/docs_upload.yml +++ b/.github/workflows/docs_upload.yml @@ -78,7 +78,7 @@ jobs: SSH_AUTH_SOCK: /tmp/ssh_agent.sock run: | if [ -n "$NAME" ]; then - mv docs-new target/docs-$NAME-$HASH + cp -r docs-new target/docs-$NAME-$HASH cd target/ isdiff=$(diff -r -x "*.zip" docs-master/ docs-$NAME-$HASH >&2; echo $?; exit 0) @@ -106,12 +106,12 @@ jobs: env: SSH_AUTH_SOCK: /tmp/ssh_agent.sock run: | - if [ "$ISTAG" ]; then + if [ "$ISTAG" = true ]; then git clone git@github.com:cvc5/docs-releases.git target-releases/ - mv docs-new target-releases/$NAME + cp -r docs-new target-releases/$NAME cd target-releases/ - git add docs-$NAME + git add $NAME git commit -m "Update docs for $NAME" git push |