case 4757 - manual revision stamp and copyright year set automatically when the manuals are built

A MkDocs hook (docs/8.0/rev_date.py), used by both manuals, replaces REV-AUTO
and YEAR-AUTO in the copyright line with the date of the last commit that
changed that manual, or today if it has uncommitted changes or git is not
available. A missing placeholder fails the strict build. The customer manual's
stamp had not been updated since 2022. The home page sentence about the stamp
no longer reads like a placeholder. Release procedure step 2, the docs
Dockerfile usage lines and .gitignore (__pycache__) follow.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

docs/8.0/rev_date.py

@@ -0,0 +1,34 @@
+# case 4757: the revision stamp and copyright year in the footer are set when a manual is built, never by hand.
+# Used by both manuals (hooks: in mkdocs.yml). In the copyright line REV-AUTO becomes REV-<date> and YEAR-AUTO
+# becomes that date's year. The date is the last commit that changed this manual (its folder, mkdocs.yml included),
+# or today if it has uncommitted changes or git is not available (e.g. a build outside the repo).
+# Both manuals build with strict: true, so a warning here fails the build: only a missing placeholder warns.
+import datetime
+import logging
+import os
+import subprocess
+
+log = logging.getLogger("mkdocs.hooks.rev_date")
+
+
+def _git(folder, *args):
+    return subprocess.run(["git", *args, "--", "."], cwd=folder, capture_output=True, text=True, check=True).stdout.strip()
+
+
+def on_config(config):
+    folder = os.path.dirname(os.path.abspath(config.config_file_path))
+    today = datetime.date.today().isoformat()
+    try:
+        rev = today if _git(folder, "status", "--porcelain") else _git(folder, "log", "-1", "--format=%cs")
+    except (OSError, subprocess.CalledProcessError):
+        log.info("git not available: revision date set to today")
+        rev = today
+    rev = rev or today
+
+    copyright = config.copyright or ""
+    for placeholder in ("REV-AUTO", "YEAR-AUTO"):
+        if placeholder not in copyright:
+            log.warning(f"{placeholder} not found in the copyright line of {config.config_file_path}")
+    config.copyright = copyright.replace("REV-AUTO", "REV-" + rev).replace("YEAR-AUTO", rev[:4])
+    log.info(f"revision stamp: {config.copyright}")
+    return config