Skip to content

Merge pull request #20 from xgdgsc/patch-7 #140

Merge pull request #20 from xgdgsc/patch-7

Merge pull request #20 from xgdgsc/patch-7 #140

Workflow file for this run

name: Build Docs
on:
push:
branches: [master]
permissions:
contents: write
jobs:
build:
runs-on: ubuntu-latest
if: "!(contains(github.event.head_commit.message, '[nobuild]'))"
steps:
- uses: actions/checkout@v3
- run: |
julia -e '
using Pkg
Pkg.add(name="DoctreePages")
using DoctreePages
github_action()
'
# 暂不推送到 github pages
# - uses: peaceiris/actions-gh-pages@v3
# with:
# github_token: ${{ secrets.GITHUB_TOKEN }}
# publish_dir: "./public"
- name: deploy to juliacn docs server
uses: easingthemes/ssh-deploy@main
with:
SSH_PRIVATE_KEY: ${{ secrets.SSH_PRIVATE_KEY }}
ARGS: "-rlgoDzvc -i --delete"
SOURCE: "./"
REMOTE_HOST: ${{ secrets.REMOTE_HOST }}
REMOTE_USER: ${{ secrets.REMOTE_USER }}
REMOTE_PORT: ${{ secrets.REMOTE_PORT }}
TARGET: ${{ secrets.REMOTE_TARGET }}