Update github actions to upload to mirror.

JuliaCN · Oct 21, 2023 · 02e1ebd · 02e1ebd
1 parent 70d522b
commit 02e1ebd
Showing 1 changed file with 19 additions and 2 deletions.
diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml
@@ -1,11 +1,10 @@
 name: Documentation
 
 on:
-  create:
-    tags:
   push:
     branches:
       - master
+  workflow_dispatch:
 
 jobs:
   HTML:
@@ -25,6 +24,15 @@ jobs:
         run: |
           julia -e 'include("contrib/build_sysimg.jl"); build_sysimg(force=true)'
           julia --project=doc/ doc/make.jl deploy
+      - name: Upload to mirror
+        uses: easingthemes/ssh-deploy@main
+        with:
+          SSH_PRIVATE_KEY: ${{ secrets.SSH_PRIVATE_KEY }}
+          ARGS: "-rlgoDzvc -i --delete"
+          SOURCE: "doc/build/"
+          REMOTE_HOST: ${{ secrets.REMOTE_HOST }}
+          REMOTE_USER: ${{ secrets.REMOTE_USER }}
+          TARGET: ${{ secrets.REMOTE_TARGET }}
   PDF:
     runs-on: ubuntu-latest
     steps:
@@ -40,4 +48,13 @@ jobs:
         with:
           name: compiled contents
           path: doc/build/*.pdf
+      - name: Upload to mirror
+        uses: easingthemes/ssh-deploy@main
+        with:
+          SSH_PRIVATE_KEY: ${{ secrets.SSH_PRIVATE_KEY }}
+          ARGS: "-rlgoDzvc -i"
+          SOURCE: "doc/build/"
+          REMOTE_HOST: ${{ secrets.REMOTE_HOST }}
+          REMOTE_USER: ${{ secrets.REMOTE_USER }}
+          TARGET: ${{ secrets.REMOTE_TARGET }}