search

coq / coq.github.io

Source files of the coq.inria.fr website
https://coq.inria.fr/
Other
15 stars 37 forks source link

Links with anchors do not redirect properly #235

Closed RalfJung closed 6 months ago

RalfJung commented 8 months ago

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 #list definition in that page.

Looks like the redirects for the website transition are not working properly with anchors?

brandenburg commented 6 months ago

I'm trying to have this fixed in coqdoc: https://github.com/coq/coq/pull/18431

RalfJung commented 6 months ago

:+1: 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.

Zimmi48 commented 6 months ago

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.)

brandenburg commented 6 months ago

I wasn't aware it's being handled in JavaScript; I presumed it's a server-side redirect. I can take a look.

brandenburg commented 6 months ago

Locally, #236 seems to do the trick.

RalfJung commented 6 months ago

Sadly github pages don't allow server-side redirects (IIUC), so a JavaScript hack was needed.