From e93fd13d1bebc1ca916033c481f3e4864a0dea11 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Mon, 1 Nov 2021 13:09:41 -0700 Subject: [PATCH] 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 | 8 ++++---- 1 file 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 -- 2.30.2