diff --git a/.github/workflows/build_doc.yml b/.github/workflows/build_doc.yml index 8f1283a2a..6b0bcfd63 100644 --- a/.github/workflows/build_doc.yml +++ b/.github/workflows/build_doc.yml @@ -38,10 +38,27 @@ jobs: - name: Build documentation run: opam exec -- make doc + - name: Upload artifact + uses: actions/upload-artifact@master + with: + name: artifact-doc + path: _build/doc + + deploy: + needs: build + runs-on: ubuntu-latest + + steps: + - name: Download artifact + uses: actions/download-artifact@master + with: + name: artifact-doc + path: build_doc + - name: Deploy uses: peaceiris/actions-gh-pages@v3 with: - publish_dir: _build/doc + publish_dir: build_doc destination_dir: dev enable_jekyll: true github_token: ${{ secrets.GITHUB_TOKEN }}