diff options
Diffstat (limited to '.github')
| -rw-r--r-- | .github/workflows/docs.yaml | 31 |
1 files changed, 31 insertions, 0 deletions
diff --git a/.github/workflows/docs.yaml b/.github/workflows/docs.yaml new file mode 100644 index 0000000000..a746ae6de3 --- /dev/null +++ b/.github/workflows/docs.yaml @@ -0,0 +1,31 @@ +name: Deploy the documentation + +on: + push: + branches: + - develop + + workflow_dispatch: + +jobs: + pages: + name: GitHub Pages + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v2 + + - name: Setup mdbook + uses: peaceiris/actions-mdbook@4b5ef36b314c2599664ca107bb8c02412548d79d # v1.1.14 + with: + mdbook-version: '0.4.9' + + - name: Build the documentation + run: mdbook build + + - name: Deploy latest documentation + uses: peaceiris/actions-gh-pages@068dc23d9710f1ba62e86896f84735d869951305 # v3.8.0 + with: + github_token: ${{ secrets.GITHUB_TOKEN }} + keep_files: true + publish_dir: ./book + destination_dir: ./develop |