Skip to content

don't rename index.html to indexpage.html in coqdocjs target

Björn Brandenburg requested to merge broken-link-in-docs into master

Fixes some broken links in the generated "pretty" documentation. There is really no reason to rename the file; it's unclear why it was ever done.

Merge request reports