Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
26 changes: 26 additions & 0 deletions scripts/build_site.py
Original file line number Diff line number Diff line change
Expand Up @@ -100,6 +100,32 @@ def build_site():
# Sort documents by number in reverse order (later ones more relevant)
xls_docs.sort(key=lambda x: int(x.number), reverse=True)

# Generate simple redirect pages so /xls-<number>.html redirects to
# the canonical document URL under /xls/<folder>.html.
redirect_template = env.get_template("redirect.html")
for doc in xls_docs:
# Redirect pages live under /xls/, next to the canonical XLS HTML files.
# For local builds (base_url == "."), use a relative URL that does *not*
# add another /xls/ segment; otherwise we create /xls/xls/<file>.html.
if base_url == ".":
# From scripts/_site/xls/xls-<number>.html → ./<folder>.html
target_url = f"./{doc.folder}.html"
else:
# On GitHub Pages, use an absolute URL with the base path.
target_url = f"{base_url}/xls/{doc.folder}.html"

redirect_html = redirect_template.render(
title=f"XLS-{doc.number}: {doc.title}",
target_url=target_url,
)

# /xls/ alias: /xls/xls-<number>.html
redirect_xls_path = site_dir / "xls" / f"xls-{doc.number}.html"
with open(redirect_xls_path, "w", encoding="utf-8") as f:
f.write(redirect_html)

print(f"Generated redirect: {redirect_xls_path} -> {target_url}")

# Group documents by category for category pages and navigation
categories = {}
for doc in xls_docs:
Expand Down
40 changes: 40 additions & 0 deletions scripts/templates/redirect.html
Original file line number Diff line number Diff line change
@@ -0,0 +1,40 @@
<!doctype html>
<html lang="en">
<head>
<meta charset="utf-8" />
<title>{{ title }}</title>
<link rel="canonical" href="{{ target_url }}" />

<!-- Perform a JS redirect as early as possible to minimize flicker. -->
<script>
// Use replace() so the redirect page is not kept in history
window.location.replace("{{ target_url }}");
</script>
<noscript>
<meta http-equiv="refresh" content="0; url={{ target_url }}" />
</noscript>

<!-- Match the site's dark background so there isn't a bright flash -->
<style>
html,
body {
margin: 0;
padding: 0;
background-color: #111112; /* var(--bg-color) from main site */
color: #ffffff;
font-family:
system-ui,
-apple-system,
BlinkMacSystemFont,
"Segoe UI",
sans-serif;
}
</style>
</head>
<body>
<p>
Redirecting to
<a href="{{ target_url }}">{{ title }}</a>...
</p>
</body>
</html>