Stream: Coq devs & plugin devs

Topic: Noise in CI logs


view this post on Zulip Gaëtan Gilbert (Sep 14 2021 at 15:10):

should we run ci with the noisier warnings disabled? they don't give us much and they make the logs harder to read
eg the instance locality warnings

view this post on Zulip Emilio Jesús Gallego Arias (Sep 14 2021 at 15:21):

I'm all for silent builds

view this post on Zulip Emilio Jesús Gallego Arias (Sep 14 2021 at 15:22):

What kind of filters do gitlab has tho?

view this post on Zulip Emilio Jesús Gallego Arias (Sep 14 2021 at 15:22):

IMHO warnings and multi-project refactoring are a use case different from CI


Last updated: Oct 15 2021 at 19:03 UTC