From 9e0b7e0a41d939a4a3103e697aba0f2a801b83ad Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 22 Jul 2024 14:06:33 +0200 Subject: [PATCH] split jobs --- .github/workflows/build_doc.yml | 19 ++++++++++++++++++- 1 file changed, 18 insertions(+), 1 deletion(-) 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 }}