The following PR is failing on the base CI run: https://github.com/coq/coq/pull/16099
The PR adds the new 817 compat file, and fails with
Error: extra files: theories/Compat/Coq817.v Makefile.doc:181: recipe for target '_build_vo/default/doc/stdlib//index-list.html' failed
trying to grok the script, I don't understand where it comes from
the file is correctly added to the template index
never mind, I can't read a git output correctly
Pierre-Marie Pédrot has marked this topic as resolved.
Last updated: May 31 2023 at 15:01 UTC