Add redirection for wiki links.

coq · Nov 13, 2023 · b7102d0 · b7102d0
1 parent 0f17e4b
commit b7102d0
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/pages/404.html b/pages/404.html
@@ -8,6 +8,7 @@
   const bugSimplifiedRegex = /^\/bug\/(.*)/;
   const bugPath = "/bugs/show_bug.cgi"
   const bugSearchRegex = /^\?id=(.*)/;
+  const wikiRegex = /^\/cocorico\/(.*)/;
   if (stdlibRegex.test(path)) {
     window.location = path.replace(stdlibRegex, "/doc/<#CURRENTVERSIONTAG>/stdlib/");
   } else if (refmanRegex.test(path)) {
@@ -35,6 +36,9 @@
   } else if (bugPath == path && bugSearchRegex.test(window.location.search)) {
     const bugId = window.location.search.match(bugSearchRegex)[1];
     window.location = "https://github.com/coq/coq/issues?q=is%3Aissue%20%22Original%20bug%20ID%3A%20BZ%23" + bugId + "%22"
+  } else if (wikiRegex.test(path)) {
+    const wikiLocation = path.match(wikiRegex)[1];
+    window.location = "https://github.com/coq/coq/wiki/" + wikiLocation
   } else {
     document.write("<h1>Not found</h1>");
   }