Stream: Coq devs & plugin devs

Topic: ✔ Weird error with documentation index script


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (May 30 2022 at 10:07):

trying to grok the script, I don't understand where it comes from

view this post on Zulip Pierre-Marie Pédrot (May 30 2022 at 10:08):

the file is correctly added to the template index

view this post on Zulip Pierre-Marie Pédrot (May 30 2022 at 10:08):

any idea?

view this post on Zulip Pierre-Marie Pédrot (May 30 2022 at 10:11):

never mind, I can't read a git output correctly

view this post on Zulip Notification Bot (May 30 2022 at 10:11):

Pierre-Marie Pédrot has marked this topic as resolved.


Last updated: Feb 06 2023 at 00:03 UTC