Stream: Coq devs & plugin devs

Topic: ✔ Add label to not run CI

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?

Gaëtan Gilbert (Jul 20 2021 at 10:07):

just let it run

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