Name the Gaming page, and stop the docs inventing names
The settings reference is generated, and a contract already fails when the committed copy is stale -- so it was current. It was also wrong: the Gaming page was documented as "Found on **gaming**" while every other group named a real page, because a routed page with no entry in PAGE_TITLES fell back to printing its own id. The staleness contract could not see it. Regenerating reproduced the same wrong file, so the copy was current and wrong at the same time -- a check that compares output against itself cannot catch a generator that is confidently mistaken. So the fallback is gone. A routed page with no title now refuses to render and says which page needs one, which is what makes the next page added here impossible to miss. Claude-Session: https://claude.ai/code/session_01Q84axqUE5inJhf5Jz9CFy1
This commit is contained in:
@@ -46,6 +46,7 @@ PAGE_TITLES = {
|
|||||||
"accessibility": "Accessibility", "power": "Power & Lock",
|
"accessibility": "Accessibility", "power": "Power & Lock",
|
||||||
"datetime": "Date & Time", "applications": "Applications",
|
"datetime": "Date & Time", "applications": "Applications",
|
||||||
"services": "System Health", "about": "About",
|
"services": "System Health", "about": "About",
|
||||||
|
"gaming": "Gaming",
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
@@ -146,6 +147,17 @@ def render(entries, routes):
|
|||||||
if not visible:
|
if not visible:
|
||||||
continue
|
continue
|
||||||
page = routes.get(group)
|
page = routes.get(group)
|
||||||
|
# A routed page with no title used to fall back to the raw page id, so
|
||||||
|
# the group "gaming" documented itself as "Found on **gaming**" while
|
||||||
|
# every other group named a real page. The staleness contract could not
|
||||||
|
# see it: regenerating reproduced the same wrong file, so the copy was
|
||||||
|
# current and wrong at once. Refusing to render is what makes the next
|
||||||
|
# page added here impossible to miss.
|
||||||
|
if page is not None and page not in PAGE_TITLES:
|
||||||
|
raise SchemaError(
|
||||||
|
f"group '{group}' routes to page '{page}', which has no entry in "
|
||||||
|
"PAGE_TITLES; add one rather than letting the id be printed as a name"
|
||||||
|
)
|
||||||
title = PAGE_TITLES.get(page, page or "—")
|
title = PAGE_TITLES.get(page, page or "—")
|
||||||
lines += [f"## {group}", "", f"Found on **{title}**.", ""]
|
lines += [f"## {group}", "", f"Found on **{title}**.", ""]
|
||||||
lines += ["| Setting | Default | What it does |", "|---|---|---|"]
|
lines += ["| Setting | Default | What it does |", "|---|---|---|"]
|
||||||
|
|||||||
+1
-1
@@ -113,7 +113,7 @@ Found on **Desktop & Dock**.
|
|||||||
|
|
||||||
## gaming
|
## gaming
|
||||||
|
|
||||||
Found on **gaming**.
|
Found on **Gaming**.
|
||||||
|
|
||||||
| Setting | Default | What it does |
|
| Setting | Default | What it does |
|
||||||
|---|---|---|
|
|---|---|---|
|
||||||
|
|||||||
Reference in New Issue
Block a user