Not sure if this is the right place to post this, but it seems all file links in deployed Stdlib coqdoc has gone dead. Compare the two following pages:
In the first link, none of the Require Export
module names are clickable. In the second link, they are. Unless this is some fluke it looks pretty serious to me - but may not be a bug with coqdoc itself, just with how stdlib documentation is deployed.
It's definitely worth opening an issue about so that we don't release 8.12.0 with this issue.
OK, I will do a report, but I unfortunately don't have time to investigate much further this week.
no worries, thanks for raising the issue anyway
if anyone not watching the Coq repo wants to follow this: https://github.com/coq/coq/issues/12699
Hi folks so we have two choices to fix this in the CI: to revert the deployment to makefile or just do a rm -rf _build
in the coqdoc job
the advantage of the latter is that is much less invasive while I prepare a fix upstream
Emilio Jesús Gallego Arias said:
Hi folks so we have two choices to fix this in the CI: to revert the deployment to makefile or just do a
rm -rf _build
in the coqdoc job
Any solution suits me.
I guess the latter solution is more future proof? No clear preference here though.
Last updated: Oct 13 2024 at 01:02 UTC