Bottom half of half the #nav links from stdlib pages can't be clicked on

[jmadiot]

From any page of the stdlib, for example this one, if one tries to click on "Documentation" or "Community" in the top nav bar, the mouse must point to the top 40% or so part of the button. Tested with chrome 88, firefox 85.0.

This is because the sidebar is on top of it:

Possible fix: in styles/barron/style.css, under #nav {, add: z-index: 1;. I would do a PR, but make && make run only gives me 404's. Maybe that's an issue as well.

[Zimmi48]

If you get 404 while testing locally, try adding an explicit .html to the page name.

[jmadiot]

Thank you @Zimmi48, indeed, I get fewer 404s. Now, all the pages concerned with this issue are generated by the repository coq/doc, however they hardcorded the path https://coq.inria.fr/sites/all/themes/coq/style.css in the .html files, and this style.css is nowhere in this present repository (different from styles/{barron,coq}/style.css). I can try to find someone who can modify this path, or hard-code the z-index trick in the .html files in the repo coq/doc, or change this hard-coded URL which might be hard-coded for a good reason... I don't know what's best.

[Zimmi48]

I have access to the server, so I've added your one-line fix to this style file. However, I do not like this situation where the files in https://coq.inria.fr/sites/all/themes/coq/ are not synchronized with any source repo. We should probably fix that, one way or another.

Note that https://github.com/coq/doc is automatically deployed from the sources in https://github.com/coq/coq, so in principle we shouldn't edit the content in this repository by hand.

[jmadiot]

Perfect, thanks! (and thanks for the note about the doc repo)

Maybe one fix about the lack of synchronisation is to replace sites/all/themes with styles in three files in this directory, so that adding one more synchronisation is not needed.

[Zimmi48]

This makes sense to me. We should just ensure these files are deployed. Currently, they are only used for local testing. Actually, I am not even sure this feature still exists / works. @gares You introduced those files, right? WDYT of deploying them with the HTML part of the stdlib doc?