Upload docs for tags to docs-releases (#7415)
authorGereon Kremer <nafur42@gmail.com>
Tue, 26 Oct 2021 12:25:00 +0000 (05:25 -0700)
committerGitHub <noreply@github.com>
Tue, 26 Oct 2021 12:25:00 +0000 (12:25 +0000)
This automatically uploads the generated docs to a new repository docs-releases (which should eventually become docs). In contrast to docs-ci, we only store docs for releases there.

.github/workflows/docs_upload.yml

index 7bdd186a1654277d0e8e25e83f58ed65ba9b4e00..9aadd66473c4b25ffc3389a08f571f3f650ba54f 100644 (file)
@@ -100,3 +100,21 @@ jobs:
           else
             echo "Ignored run"
           fi
+
+      - name: Update docs for release
+        continue-on-error: true
+        env:
+            SSH_AUTH_SOCK: /tmp/ssh_agent.sock
+        run: |
+          if [ "$ISTAG" ]; then
+            git clone git@github.com:cvc5/docs-releases.git target-releases/
+            mv docs-new target-releases/$NAME
+            cd target-releases/
+
+            git add docs-$NAME
+
+            git commit -m "Update docs for $NAME"
+            git push
+          else
+            echo "Ignored run"
+          fi