Add handling for the /distrib/current/ sub-paths.

coq · Oct 12, 2023 · 9ec0e10 · 9ec0e10
1 parent 5038407
commit 9ec0e10
Showing 1 changed file with 12 additions and 2 deletions.
diff --git a/pages/404.html b/pages/404.html
@@ -8,10 +8,20 @@
     window.location = path.replace(stdlibRegex, "/doc/<#CURRENTVERSIONTAG>/stdlib/");
   } else if (refmanRegex.test(path)) {
     const version = path.match(refmanRegex)[1];
-    window.location = path.replace(refmanRegex, "/doc/" + version + "/refman/");
+    if (version == "current") {
+      window.location = path.replace(refmanRegex, "/doc/<#CURRENTVERSIONTAG>/refman/");
+    }
+    else {
+      window.location = path.replace(refmanRegex, "/doc/" + version + "/refman/");
+    }
   } else if (stdlibDistribRegex.test(path)) {
     const version = path.match(stdlibDistribRegex)[1];
-    window.location = path.replace(stdlibDistribRegex, "/doc/" + version + "/stdlib/");
+    if (version == "current") {
+      window.location = path.replace(stdlibDistribRegex, "/doc/<#CURRENTVERSIONTAG>/stdlib/");
+    }
+    else {
+      window.location = path.replace(stdlibDistribRegex, "/doc/" + version + "/stdlib/");
+    }
   } else {
     document.write("<h1>Not found</h1>");
   }