From 4602f5fefb7b58d9d4c0ce8d818c9713add825a5 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:21:45 +0100
Subject: [PATCH 1/2] let `make run` serve 404.html

---
 srv/server.py | 20 +++++++++++++++++---
 1 file changed, 17 insertions(+), 3 deletions(-)

diff --git a/srv/server.py b/srv/server.py
index e831e75d0c..ce484b30b1 100644
--- a/srv/server.py
+++ b/srv/server.py
@@ -1,10 +1,24 @@
-import http.server
-from http.server import HTTPServer, BaseHTTPRequestHandler
+from http.server import SimpleHTTPRequestHandler
 import socketserver
 
 PORT = 8000
 
-Handler = http.server.SimpleHTTPRequestHandler
+
+class Handler(SimpleHTTPRequestHandler):
+    def send_error(self, code, message=None):
+        if code == 404:
+            with open("404.html", "rb") as err_msg:
+                page404 = err_msg.read()
+
+            self.send_response(code)
+            self.send_header("Connection", "close")
+            self.send_header("Content-Type", "text/html")
+            self.send_header("Content-Length", str(len(page404)))
+            self.end_headers()
+            self.wfile.write(page404)
+        else:
+            SimpleHTTPRequestHandler.send_error(self, code, message)
+
 
 Handler.extensions_map={
     '.manifest': 'text/cache-manifest',

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 2/2] 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