Skip to content

Commit

Permalink
propagate hash fragment (=href anchor) when redirecting URLs
Browse files Browse the repository at this point in the history
When redirecting requests for stdlib or refman pages, propagate the
URL's fragment identifer (the string following the '#' sign, if any).

This is required for stdlib URLs so that links generated by coqdoc
resolve to specifc identifiers, as intended.

While at it, also preserve the fragment identifier in refman pages, in
case someone, somewhere meant to link to specific parts of the
reference manual.

Fixes: #235
  • Loading branch information
brandenburg committed Dec 21, 2023
1 parent 4602f5f commit a6a0337
Showing 1 changed file with 7 additions and 6 deletions.
13 changes: 7 additions & 6 deletions pages/404.html
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
<#include "incl/macros.html">
<script>
const path = window.location.pathname;
const hash = window.location.hash;
const stdlibRegex = /^\/(stdlib|library)\//;
const refmanRegex = /^\/distrib\/(.*)\/refman\//;
const V80refmanRegex = /^\/distrib\/V8.0\/doc\//;
Expand All @@ -10,25 +11,25 @@
const bugSearchRegex = /^\?id=(.*)/;
const wikiRegex = /^\/cocorico\/(.*)/;
if (stdlibRegex.test(path)) {
window.location = path.replace(stdlibRegex, "/doc/<#CURRENTVERSIONTAG>/stdlib/");
window.location = path.replace(stdlibRegex, "/doc/<#CURRENTVERSIONTAG>/stdlib/") + hash;
} else if (refmanRegex.test(path)) {
const version = path.match(refmanRegex)[1];
if (version == "current") {
window.location = path.replace(refmanRegex, "/doc/<#CURRENTVERSIONTAG>/refman/");
window.location = path.replace(refmanRegex, "/doc/<#CURRENTVERSIONTAG>/refman/") + hash;
}
else {
window.location = path.replace(refmanRegex, "/doc/" + version + "/refman/");
window.location = path.replace(refmanRegex, "/doc/" + version + "/refman/") + hash;
}
} else if (stdlibDistribRegex.test(path)) {
const version = path.match(stdlibDistribRegex)[1];
if (version == "current") {
window.location = path.replace(stdlibDistribRegex, "/doc/<#CURRENTVERSIONTAG>/stdlib/");
window.location = path.replace(stdlibDistribRegex, "/doc/<#CURRENTVERSIONTAG>/stdlib/") + hash;
}
else {
window.location = path.replace(stdlibDistribRegex, "/doc/" + version + "/stdlib/");
window.location = path.replace(stdlibDistribRegex, "/doc/" + version + "/stdlib/") + hash;
}
} else if (V80refmanRegex.test(path)) {
window.location = path.replace(V80refmanRegex, "/doc/V8.0/doc/");
window.location = path.replace(V80refmanRegex, "/doc/V8.0/doc/") + hash;
} else if (bugSimplifiedRegex.test(path)) {
const bugId = path.match(bugSimplifiedRegex)[1];
// To avoid having to rely on the correspondence table from the migration, we redirect to the search page
Expand Down

0 comments on commit a6a0337

Please sign in to comment.