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
|
