Links with anchors do not redirect properly #235
Comments
brandenburg
added a commit
to brandenburg/coq
that referenced
this issue
Dec 21, 2023
The reference manual and the standard library documentation have moved on the Coq homepage. The URLs are now `https://coq.inria.fr/doc/V${VERSION}/refman/` and `https://coq.inria.fr/doc/V${VERSION}/stdlib/`, respectively. While there is an automatic redirect from the old URL to the new one, the redirect breaks the anchors that `coqdoc` uses to refer to specific symbols. To avoid the problem, this patch updates the configuration to link to the actual URL instead to avoid the anchor-breaking redirect. See also: coq/coq.github.io#235
|
I'm trying to have this fixed in |
|
👍 on fixing newly generated docs to not rely on the redirects, but given there are already tons of links out there, I don't think think that should be considered as fixing this issue. |
|
It seems like the JS code that handles the redirects could be adapted to preserve the anchors. Anyone wants to have a try? (If it has to be me, it will take more than a month before I can fix this, even though it likely is a very easy fix.) |
|
I wasn't aware it's being handled in JavaScript; I presumed it's a server-side redirect. I can take a look. |
brandenburg
added a commit
to brandenburg/coq.github.io
that referenced
this issue
Dec 21, 2023
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: coq#235
|
Locally, #236 seems to do the trick. |
|
Sadly github pages don't allow server-side redirects (IIUC), so a JavaScript hack was needed. |
SkySkimmer
pushed a commit
to SkySkimmer/coq
that referenced
this issue
Jan 10, 2024
The reference manual and the standard library documentation have moved on the Coq homepage. The URLs are now `https://coq.inria.fr/doc/V${VERSION}/refman/` and `https://coq.inria.fr/doc/V${VERSION}/stdlib/`, respectively. While there is an automatic redirect from the old URL to the new one, the redirect breaks the anchors that `coqdoc` uses to refer to specific symbols. To avoid the problem, this patch updates the configuration to link to the actual URL instead to avoid the anchor-breaking redirect. See also: coq/coq.github.io#235 (cherry picked from commit b21e7af)
louiseddp
pushed a commit
to louiseddp/coq
that referenced
this issue
Feb 27, 2024
The reference manual and the standard library documentation have moved on the Coq homepage. The URLs are now `https://coq.inria.fr/doc/V${VERSION}/refman/` and `https://coq.inria.fr/doc/V${VERSION}/stdlib/`, respectively. While there is an automatic redirect from the old URL to the new one, the redirect breaks the anchors that `coqdoc` uses to refer to specific symbols. To avoid the problem, this patch updates the configuration to link to the actual URL instead to avoid the anchor-breaking redirect. See also: coq/coq.github.io#235
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
coqdoc generates links to URLs like http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Init.Datatypes.html#list. However, those URLs do not work properly any more: they do go to the page for
Coq.Init.Datatypes, but they don't jump to the#listdefinition in that page.Looks like the redirects for the website transition are not working properly with anchors?
The text was updated successfully, but these errors were encountered: