Is it difficult to match pages between the versions of the refman? I very often want to look at more recent documentation when googling stuff, but this always brings me to the homepage. Is it possible to keep the page?
The widget was introduced by @Clément Pit-Claudel. I haven't dug into how it works. However, matching pages across versions should be easy. Especially given that when pages were renamed / split, we've introduced redirections for old links to continue to work (except the anchors).
For instance, https://coq.inria.fr/refman/language/gallina-specification-language.html redirects to https://coq.inria.fr/refman/language/core/index.html or https://coq.inria.fr/refman/addendum/canonical-structures.html redirects to https://coq.inria.fr/refman/language/extensions/canonical.html.
Right, but what about pages which get moved/deleted
I guess we could always fallback on the home page
There is always an appropriate fallback. In the first example I gave, the two pages do not match exactly. The first one was split into multiple pages. So it redirects to the most appropriate fallback.
But yeah, in the end the ultimate fallback is the home page
Do we have to specify all the "links" by hand?
I have no idea how this widget works, but if someone knows and I just have to provide a list of renamed pages, I am ready to do this work.
It wouldn't take me so long, as I know what has changed quite well.
OK I'll create an issue on github so we can work on it soon
Last updated: Feb 01 2023 at 13:03 UTC