Stream: Coq devs & plugin devs

Topic: Why is coqtail failing in ci?


view this post on Zulip Ali Caglayan (Aug 24 2020 at 04:10):

The coqtail repo seems to be passing, but it fails in the coq CI. I can't seem to find when this started happening. All I know is that it has happened in #12878 and #12879. The error that gets thrown is ERROR: file not found: tests/test_coqtop.py.

Anybody know what is going on?

view this post on Zulip Gaƫtan Gilbert (Aug 24 2020 at 06:36):

because of https://github.com/whonore/Coqtail/pull/134 which renamed the test directory afaict

view this post on Zulip Wolf Honore (Aug 24 2020 at 18:21):

Sorry about that. https://github.com/coq/coq/pull/12886 should fix it.


Last updated: Oct 16 2021 at 03:02 UTC