From 509eda5ac6dce53afbbf658ac540bec7155153f2 Mon Sep 17 00:00:00 2001
From: Mike Langmayr <1809691+mikelangmayr@users.noreply.github.com>
Date: Wed, 23 Sep 2026 13:51:55 -0700
Subject: [PATCH] Stop cancelling the docs publish and keep the build cache out
 of the site

---
 .github/workflows/docs.yml | 12 ++++++++----
 docs/development/index.md  |  4 +++-
 2 files changed, 11 insertions(+), 5 deletions(-)

diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml
index f989f51..6211a93 100644
--- a/.github/workflows/docs.yml
+++ b/.github/workflows/docs.yml
@@ -7,10 +7,11 @@ on:
     types: [opened, synchronize, reopened, closed]
   workflow_dispatch:
 
-# Serialize per ref so a rapid second push cannot race the first one's gh-pages commit
+# Serialize per ref so a rapid second push cannot race the first one's gh-pages commit. Only pull
+# request builds are superseded; cancelling a publish would leave the site unbuilt.
 concurrency:
   group: docs-${{ github.ref }}
-  cancel-in-progress: true
+  cancel-in-progress: ${{ github.event_name == 'pull_request' }}
 
 permissions:
   contents: write
@@ -58,7 +59,7 @@ jobs:
       - name: Build documentation
         run: |
           python -c "import camera_interface; print(camera_interface.instrument_name())"
-          sphinx-build -W -b html docs docs/_build/html
+          sphinx-build -W -b html -d docs/_build/doctrees docs docs/_build/html
           touch docs/_build/html/.nojekyll
 
       - name: Upload rendered site
@@ -68,8 +69,11 @@ jobs:
           path: docs/_build/html
           retention-days: 14
 
+      # workflow_dispatch publishes too, so the site can be restored without an empty commit
       - name: Publish to the site root
-        if: github.event_name == 'push' && github.ref == 'refs/heads/main'
+        if: >
+          github.ref == 'refs/heads/main' &&
+          (github.event_name == 'push' || github.event_name == 'workflow_dispatch')
         uses: peaceiris/actions-gh-pages@v4
         with:
           github_token: ${{ secrets.GITHUB_TOKEN }}
diff --git a/docs/development/index.md b/docs/development/index.md
index b48c396..71d3397 100644
--- a/docs/development/index.md
+++ b/docs/development/index.md
@@ -4,9 +4,11 @@
 
 ```bash
 pip install -r docs/requirements.txt
-sphinx-build -W -b html docs docs/_build/html
+sphinx-build -W -b html -d docs/_build/doctrees docs docs/_build/html
 ```
 
+`-d` keeps Sphinx's build cache out of the output directory, which is published verbatim.
+
 `-W` turns warnings into errors, which is what CI uses, so a broken cross-reference fails the build
 rather than shipping a dead link.