Merge remote-tracking branch 'origin/docs/publish_docs' into develop

Author: mdelmans

.github/workflows/chore.yml

@@ -23,7 +23,7 @@ jobs:
         run: |
           git config --global user.name "bot"
           git config --global user.email "bot@colorifix.com"
-          git fetch origin
+          git fetch
           git checkout develop
           git merge --no-ff origin/${{ github.event.pull_request.head.ref }} -m "Merge ${{ github.event.pull_request.head.ref }} into develop"
           git push origin develop