From fac0f6b94290ab567a15d65199767f0191d63d87 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Wed, 4 Feb 2026 20:04:41 +0000
Subject: [PATCH 1/2] Initial plan


From 0e81c0ac11927d3652c948d721a654f5d14ec686 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Wed, 4 Feb 2026 20:06:03 +0000
Subject: [PATCH 2/2] Fix CI: Only deploy docs on master push, not on PRs

Co-authored-by: pgit <1456612+pgit@users.noreply.github.com>
---
 .github/workflows/gh-pages.yml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.github/workflows/gh-pages.yml b/.github/workflows/gh-pages.yml
index 1e7132b..5aa2f46 100644
--- a/.github/workflows/gh-pages.yml
+++ b/.github/workflows/gh-pages.yml
@@ -38,6 +38,7 @@ jobs:
           make html
 
       - name: Deploy to GitHub Pages
+        if: github.event_name == 'push' && github.ref == 'refs/heads/master'
         uses: peaceiris/actions-gh-pages@v3
         with:
           github_token: ${{ secrets.GITHUB_TOKEN }}