ci: correct the duplicate-build diagnosis

The previous commit blamed `actions/checkout` for not fetching tags. It does
(with `fetch-depth: 0`), and the run logs show it: the v1.9.1 master run's
checkout fetched every tag up to v1.9.0 and nothing newer, because v1.9.1 did
not exist on the remote yet — the branch push came first, the tag push eight
seconds later. The duplicate is a race with the tag push, not a missing
fetch. Comments corrected; the re-fetch before the decision stays, and it is
what makes the gap between the checkout and the decision irrelevant (the tag
only has to exist by the time *this* step runs).

.github/workflows/docker.yml

@@ -39,10 +39,9 @@ concurrency:
 jobs:
   # A tag push and a branch push to the same commit fire two workflow runs;
   # build only once. Tag runs always build; master runs build only when the
-  # pushed commit is not already tagged (the tag run covers it) — which needs
-  # the tags to be present and to have been pushed by the time this runs, so
-  # `docker.yml`'s check step fetches them and the release flow pushes both
-  # refs together.
+  # pushed commit is not already tagged (the tag run covers it). That check
+  # can only see tags that already exist on the remote — see the check step's
+  # re-fetch and the one-push release flow in AGENTS.md.
   should-build:
     runs-on: ubuntu-latest
     timeout-minutes: 10
@@ -77,14 +76,16 @@ jobs:
         shell: bash
         run: |
           if [ "$GITHUB_REF_TYPE" = "branch" ]; then
-            # The check below is only as good as the tags in this clone, and
-            # `actions/checkout` does not fetch them (fetch-tags defaults to
-            # false, and fetch-depth does not imply it) — which is why the
-            # master run used to build the very commit the tag run was building
-            # in parallel. Fetched here, right before the decision, so a tag
-            # pushed moments ago is seen too. A tag pushed *after* this run
-            # started cannot be anticipated: push the branch and the tag
-            # together (`git push origin master v1.9.1`) or the tag first.
+            # A branch run can start before the release tag for its commit
+            # reaches the remote — pushing master first is the usual way to hit
+            # it — and then `git tag --points-at` legitimately finds nothing
+            # and this run builds the same commit the tag run is building: two
+            # docker builds, one release. (Seen on v1.9.0 and v1.9.1: the
+            # branch run's checkout had every tag *except* the one being
+            # pushed.) Re-fetching here, immediately before the decision,
+            # shrinks the window to "the tag was pushed after this step ran";
+            # pushing the branch and the tag together
+            # (`git push origin master vX.Y.Z`) removes it.
             git fetch --tags --force --quiet origin
           fi
           if [ "$GITHUB_REF_TYPE" = "branch" ] && git tag --points-at "$GITHUB_SHA" | grep -q .; then