Merge branch 'master' into there_are_no_extra_allocations

Author: Christian-B

.github/workflows/publish.yml

@@ -59,7 +59,7 @@ jobs:
           cp -vaT $ROOT_DOC_DIR $DEPLOY_DIR
           cp -vaT $C_DOC_DIR $DEPLOY_DIR/c
       - name: Deploy to GitHub Pages
-        uses: JamesIves/github-pages-deploy-action@v4.7.2
+        uses: JamesIves/github-pages-deploy-action@v4.7.3
         with:
           branch: gh-pages
           folder: ${{ env.DEPLOY_DIR }}