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/

Anybody know what is going on?

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

because of which renamed the test directory afaict

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

Sorry about that. should fix it.

Last updated: Oct 16 2021 at 03:02 UTC