Something is wrong with https://coq.inria.fr/refman

[Zimmi48]

As notice by @kyoDralliam, https://coq.inria.fr/refman seems to be displayed without any CSS, whereas https://coq.inria.fr/refman/ looks good.

Note that the same is true for https://coq.inria.fr/distrib/current/refman vs https://coq.inria.fr/distrib/current/refman/. Unfortunately, it is to the former that the official website points so it is likely that people are going to encounter the problem soon. I'm going to push a commit adding the trailing dot to the links as a temporary workaround.

[kyoDralliam]

I think the "real issue" is rather that all links on the page return a 404 (that's probably the reason there is no displayed CSS).

[Zimmi48]

OK, indeed. Because of this missing /, the relative links are all interpreted relative to https://coq.inria.fr/distrib/current/ instead of being relative to https://coq.inria.fr/distrib/current/refman/, which makes them 404.
The bug was not there before because of a (visible) redirection from e.g. https://coq.inria.fr/distrib/V8.9.0/refman to https://coq.inria.fr/distrib/V8.9.0/refman/. @maximedenes Would it be possible to emulate the same thing?

[maximedenes]

I think so. What kind of redirection do you want?

[Zimmi48]

From https://coq.inria.fr/distrib/current/refman to https://coq.inria.fr/distrib/current/refman/ and from https://coq.inria.fr/refman to https://coq.inria.fr/refman/

[Zimmi48]

@maximedenes If this is not too hard to set up, I think this should get quite a high priority. Until a few days ago, the URL without the ending slash was the one that was linked to from the main page of the website. It is not unlikely that some users have saved this URL in their bookmarks.

[maximedenes]

From https://coq.inria.fr/distrib/current/refman to https://coq.inria.fr/distrib/current/refman/ and from https://coq.inria.fr/refman to https://coq.inria.fr/refman/

Yes, but what code?

[maximedenes]

301?

[maximedenes]

Ok, in fact I didn't have to add a redirection, there was already one. It was simply masked by the reverse proxy. Now fixed.

[Zimmi48]

Thanks again!