diff --git a/pages/404.html b/pages/404.html index bb1d22f77e..6876bb68ee 100644 --- 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("