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)
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

index 9aadd66473c4b25ffc3389a08f571f3f650ba54f..fd489beeef14f8329b281ceb8b2d702b7fce89e9 100644 (file)
@@ -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