From d30d1f93cf77f52177538f61595bb6730089bee4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= <theo.zimmermann@telecom-paris.fr>
Date: Wed, 31 Jan 2024 14:06:55 +0100
Subject: [PATCH] Redirect /refman to current version of refman with explicit
 version.

As discussed in coq/coq#18547 and coq/coq.github.io#233.
Fixes coq/coq.github.io#238.
---
 pages/404.html | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/pages/404.html b/pages/404.html
index d56c943de3..206ae8c03f 100644
--- a/pages/404.html
+++ b/pages/404.html
@@ -2,17 +2,21 @@
 <script>
   const path = window.location.pathname;
   const hash = window.location.hash;
+  const refmanRegex = /^\/refman/;
   const stdlibRegex = /^\/(stdlib|library)\//;
-  const refmanRegex = /^\/distrib\/(.*)\/refman\//;
+  const refmanDistribRegex = /^\/distrib\/(.*)\/refman\//;
   const V80refmanRegex = /^\/distrib\/V8.0\/doc\//;
   const stdlibDistribRegex = /^\/distrib\/(.*)\/stdlib\//;
   const bugSimplifiedRegex = /^\/bug\/(.*)/;
   const bugPath = "/bugs/show_bug.cgi"
   const bugSearchRegex = /^\?id=(.*)/;
   const wikiRegex = /^\/cocorico\/(.*)/;
-  if (stdlibRegex.test(path)) {
+  if (refmanRegex.test(path)) {
+    window.location = path.replace(refmanRegex, "/doc/<#CURRENTVERSIONTAG>/refman") + hash;
+  }
+  else if (stdlibRegex.test(path)) {
     window.location = path.replace(stdlibRegex, "/doc/<#CURRENTVERSIONTAG>/stdlib/") + hash;
-  } else if (refmanRegex.test(path)) {
+  } else if (refmanDistribRegex.test(path)) {
     const version = path.match(refmanRegex)[1];
     if (version == "current") {
       window.location = path.replace(refmanRegex, "/doc/<#CURRENTVERSIONTAG>/refman/") + hash;