From a26c1489dc07881dfb624a3fc0f5949dd6951841 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Rapha=C3=ABl=20de=20Courville?= <groupes.raphael@gmail.com>
Date: Wed, 11 Dec 2024 13:40:09 +0100
Subject: [PATCH] Add deployment step for Javadoc to GitHub Pages (instead of
 deploy from branch)

---
 .github/workflows/build-and-deploy-javadoc.yml | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/.github/workflows/build-and-deploy-javadoc.yml b/.github/workflows/build-and-deploy-javadoc.yml
index 63c55f5..734f969 100644
--- a/.github/workflows/build-and-deploy-javadoc.yml
+++ b/.github/workflows/build-and-deploy-javadoc.yml
@@ -114,3 +114,21 @@ jobs:
         fi
       env:
         PAT_TOKEN: ${{ secrets.PAT_TOKEN }}
+
+  deploy-javadoc:
+    runs-on: ubuntu-latest
+    needs: commit-javadoc
+
+    steps:
+    - name: Checkout gh-pages branch
+      uses: actions/checkout@v3
+      with:
+        repository: processing/processing4-javadocs
+        ref: gh-pages
+        fetch-depth: 0
+
+    - name: Deploy to GitHub Pages
+      uses: peaceiris/actions-gh-pages@v3
+      with:
+        github_token: ${{ secrets.GITHUB_TOKEN }}
+        publish_dir: ./docs