From 89ab2efc69b260ca54404f4650f37bbcd51f48ad Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Thu, 28 Mar 2024 15:34:39 +0100 Subject: [PATCH] Plublish doc on gh-pages branch Use a specific branch to deploy the documentation. --- .github/workflows/documentation.yml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/.github/workflows/documentation.yml b/.github/workflows/documentation.yml index 0fa5ba3..72f4201 100644 --- a/.github/workflows/documentation.yml +++ b/.github/workflows/documentation.yml @@ -10,8 +10,7 @@ env: OPAMYES: true jobs: - odoc: - name: Odoc documentation + build-and-deploy: runs-on: ubuntu-latest env: OPAMWITHDOC: true @@ -33,8 +32,9 @@ jobs: - name: Make odoc documentation run: opam exec -- make doc - - name: Upload documentation - uses: actions/upload-artifact@v4 + - name: Deploy + uses: JamesIves/github-pages-deploy-action@v4 with: - name: odoc - path: _build/default/_doc/_html/ + token: ${{ secrets.GITHUB_TOKEN }} + branch: gh-pages + folder: _build/default/_doc/_html/