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


Last updated: Oct 21 2021 at 22:02 UTC