Merge remote-tracking branch 'origin/main' into publication

Author: Azure Pipelines

.github/workflows/docs-deploy.yml

@@ -79,7 +79,7 @@ jobs:
 
       - name: Deploy 🚀
         if: ${{ github.event_name != 'pull_request' }}
-        uses: JamesIves/github-pages-deploy-action@v4.6.8
+        uses: JamesIves/github-pages-deploy-action@v4.7.1
         with:
           token: ${{ secrets.GITHUB_TOKEN }}
           branch: gh-pages # The branch the action should deploy to.