Deploy docs only when merged into master

Author: andreasabel

.github/workflows/docs.yml

@@ -52,6 +52,7 @@ jobs:
 
       - name: Deploy to GitHub Pages
         uses: peaceiris/actions-gh-pages@v4
+        if: github.ref == 'refs/heads/master'
         with:
           github_token: ${{ secrets.GITHUB_TOKEN }}
           publish_dir: ${{ env.DOCS_BUILD_HTML_DIR }}