Redirect /refman to current version of refman with explicit version.

As discussed in coq/coq#18547 and #233. Fixes #238.
coq · Jan 31, 2024 · d30d1f9 · d30d1f9
1 parent 8030543
commit d30d1f9
Showing 1 changed file with 7 additions and 3 deletions.
diff --git 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;