search

coq / coq.github.io

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

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

Closed Zimmi48 closed 5 years ago

Zimmi48 commented 5 years ago

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 commented 5 years ago

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 commented 5 years ago

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 commented 5 years ago

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

Zimmi48 commented 5 years ago

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 commented 5 years ago

@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 commented 5 years ago

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 commented 5 years ago

301?

maximedenes commented 5 years ago

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 commented 5 years ago

Thanks again!