Pierre-Marie Pédrot (May 30 2022 at 10:06): Pierre-Marie Pédrot (May 30 2022 at 10:06):The following PR is failing on the base CI run: https://github.com/coq/coq/pull/16099
Pierre-Marie Pédrot (May 30 2022 at 10:06):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
Pierre-Marie Pédrot (May 30 2022 at 10:08):the file is correctly added to the template index
Pierre-Marie Pédrot (May 30 2022 at 10:08):any idea?
Pierre-Marie Pédrot (May 30 2022 at 10:11):never mind, I can't read a git output correctly
Notification Bot (May 30 2022 at 10:11):Pierre-Marie Pédrot has marked this topic as resolved.
Last updated: May 31 2023 at 15:01 UTC