Stream: Coq devs & plugin devs

Topic: ✔ Add label to not run CI

view this post on Zulip Ali Caglayan (Jul 20 2021 at 09:57):

Some PRs, especially (github) documentation PRs, don't really need the CI to be run, as a result every time there is a push it tends to get manually cancelled. Perhaps we can make a label so that the CI doesn't get run?

view this post on Zulip Gaëtan Gilbert (Jul 20 2021 at 10:07):

just let it run

view this post on Zulip Notification Bot (Jul 20 2021 at 12:25):

Ali Caglayan has marked this topic as resolved.

Last updated: Dec 05 2023 at 12:01 UTC