From a6a03376dcbafc71596b5417c01c17359cd09fca Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Thu, 21 Dec 2023 22:41:27 +0100
Subject: [PATCH] propagate hash fragment (=href anchor) when redirecting URLs

When redirecting requests for stdlib or refman pages, propagate the
URL's fragment identifer (the string following the '#' sign, if any).

This is required for stdlib URLs so that links generated by coqdoc
resolve to specifc identifiers, as intended.

While at it, also preserve the fragment identifier in refman pages, in
case someone, somewhere meant to link to specific parts of the
reference manual.

Fixes: https://github.com/coq/coq.github.io/issues/235
---
 pages/404.html | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

diff --git a/pages/404.html b/pages/404.html
index 6876bb68ee..d56c943de3 100644
--- a/pages/404.html
+++ b/pages/404.html
@@ -1,6 +1,7 @@
 <#include "incl/macros.html">
 <script>
   const path = window.location.pathname;
+  const hash = window.location.hash;
   const stdlibRegex = /^\/(stdlib|library)\//;
   const refmanRegex = /^\/distrib\/(.*)\/refman\//;
   const V80refmanRegex = /^\/distrib\/V8.0\/doc\//;
@@ -10,25 +11,25 @@
   const bugSearchRegex = /^\?id=(.*)/;
   const wikiRegex = /^\/cocorico\/(.*)/;
   if (stdlibRegex.test(path)) {
-    window.location = path.replace(stdlibRegex, "/doc/<#CURRENTVERSIONTAG>/stdlib/");
+    window.location = path.replace(stdlibRegex, "/doc/<#CURRENTVERSIONTAG>/stdlib/") + hash;
   } else if (refmanRegex.test(path)) {
     const version = path.match(refmanRegex)[1];
     if (version == "current") {
-      window.location = path.replace(refmanRegex, "/doc/<#CURRENTVERSIONTAG>/refman/");
+      window.location = path.replace(refmanRegex, "/doc/<#CURRENTVERSIONTAG>/refman/") + hash;
     }
     else {
-      window.location = path.replace(refmanRegex, "/doc/" + version + "/refman/");
+      window.location = path.replace(refmanRegex, "/doc/" + version + "/refman/") + hash;
     }
   } else if (stdlibDistribRegex.test(path)) {
     const version = path.match(stdlibDistribRegex)[1];
     if (version == "current") {
-      window.location = path.replace(stdlibDistribRegex, "/doc/<#CURRENTVERSIONTAG>/stdlib/");
+      window.location = path.replace(stdlibDistribRegex, "/doc/<#CURRENTVERSIONTAG>/stdlib/") + hash;
     }
     else {
-      window.location = path.replace(stdlibDistribRegex, "/doc/" + version + "/stdlib/");
+      window.location = path.replace(stdlibDistribRegex, "/doc/" + version + "/stdlib/") + hash;
     }
   } else if (V80refmanRegex.test(path)) {
-    window.location = path.replace(V80refmanRegex, "/doc/V8.0/doc/");
+    window.location = path.replace(V80refmanRegex, "/doc/V8.0/doc/") + hash;
   } else if (bugSimplifiedRegex.test(path)) {
     const bugId = path.match(bugSimplifiedRegex)[1];
     // To avoid having to rely on the correspondence table from the migration, we redirect to the search page