fix: skip the static-site sync when a release changes no page

Author: marc0olo

.github/workflows/sync-static-site.yml

@@ -96,18 +96,34 @@ jobs:
             git push origin --delete "$BRANCH"
           fi
 
-          # A release that ships canister changes without touching docs/ leaves
-          # the synced pages byte-identical, so there is no content to review.
-          # The pin still has to move: it is allowed to sit on a commit only
-          # while no release carries the pages, and skipping here would strand
-          # it on that commit for good. So the PR is opened either way, and the
-          # body says which of the two it is.
           CHANGED=$(git -C /tmp/certified-assets diff --name-only "${PIN}..${TAG}" -- docs/)
-          echo "needed=true" >> $GITHUB_OUTPUT
           if [ -z "$CHANGED" ]; then
-            echo "No docs/ changes between $PIN and $TAG: advancing the pin only."
-            echo "pin_only=true" >> $GITHUB_OUTPUT
+            # A release that ships canister changes without touching docs/ leaves
+            # the synced pages byte-identical, so there is nothing to review. Two
+            # cases, and only one of them is worth a pull request.
+            if [ -n "$INPUT_REF" ] || ! git -C /tmp/certified-assets show-ref \
+                 --verify --quiet "refs/tags/${PIN}"; then
+              # The pin is a commit (or a ref was dispatched by hand). Moving it
+              # onto the tag is the point: a commit pin is allowed only while no
+              # release carries the pages, and skipping here would strand it
+              # there for good.
+              echo "No docs/ changes between $PIN and $TAG: advancing the pin only."
+              echo "needed=true" >> $GITHUB_OUTPUT
+              echo "pin_only=true" >> $GITHUB_OUTPUT
+            else
+              # The pin is already a tag, so a pull request would carry an empty
+              # page diff and a bumped ref, for a reader to review and merge with
+              # nothing in it. The pin lags the release and stays accurate: it
+              # says which ref this copy came from, and the copy still matches it.
+              # The release itself is not lost, since the recipe that deploys this
+              # canister releases in lockstep and is tracked under `watched`.
+              echo "No docs/ changes between $PIN and $TAG, and the pin is a tag."
+              echo "Nothing to sync."
+              echo "needed=false" >> $GITHUB_OUTPUT
+              exit 0
+            fi
           else
+            echo "needed=true" >> $GITHUB_OUTPUT
             echo "Changed upstream pages:"
             echo "$CHANGED"
             echo "pin_only=false" >> $GITHUB_OUTPUT

.sources/upstream.json

@@ -65,6 +65,11 @@
         "range contains before pinning past a tag, and prefer a tag whenever one",
         "carries the pages. The sync workflow moves the pin onto a tag at the next",
         "release even when no page changed, so a commit pin is never permanent.",
+        "Once it is a tag, a release that changes no page is skipped instead: the",
+        "pin then lags the latest release and stays accurate, since it records the",
+        "ref this copy came from and the copy still matches it. The release is not",
+        "missed either way, because the recipe that deploys this canister releases",
+        "in lockstep and is tracked under `watched`.",
         "History: the first sync used d9cb7df, because certified-assets#124 landed",
         "the frontmatter contract this sync requires after the v0.3.3 tag."
       ]