fix: force docs to point to dev docs (#420)

Author: RobPasMue

.github/workflows/ci-build.yml

@@ -150,6 +150,11 @@ jobs:
             cname: ${{ env.DOCUMENTATION_CNAME }}
             token: ${{ secrets.GITHUB_TOKEN }}
 
+  adapt-landing-page-dev:
+    uses: ./.github/workflows/update-gh-pages.yml
+    needs: [doc-deploy-dev]
+    secrets: inherit
+
   doc-index-dev:
     name: "Deploy dev docs index"
     if: github.ref == 'refs/heads/main'
@@ -205,6 +210,11 @@ jobs:
           cname: ${{ env.DOCUMENTATION_CNAME }}
           token: ${{ secrets.GITHUB_TOKEN }}
 
+  adapt-landing-page-release:
+    uses: ./.github/workflows/update-gh-pages.yml
+    needs: [docs-release]
+    secrets: inherit
+
   doc-index-release:
     name: "Deploy release docs index"
     runs-on: ubuntu-latest

.github/workflows/update-gh-pages.yml

@@ -0,0 +1,26 @@
+
+name: Update index.html in GH Pages
+
+on:
+  workflow_dispatch:
+  workflow_call:
+
+jobs:
+  update-gh-pages:
+    runs-on: ubuntu-latest
+
+    steps:
+    - name: Checkout repository
+      uses: actions/checkout@v4
+      with:
+        ref: gh-pages
+
+    - name: Replace 'version/stable' with 'version/dev' in index.html
+      run: |
+        sed -i 's/version\/stable/version\/dev/g' index.html
+
+    - name: "Commit changes"
+      uses: EndBug/add-and-commit@v9
+      with:
+        default_author: github_actions
+        message: "update index.html"