Skip to content

Commit

Permalink
ci: do not let bors run if the awaiting-CI label is present (#6068)
Browse files Browse the repository at this point in the history
We already did this in mathlib3.

This forward-ports leanprover-community/mathlib#9478, which was created a few days after this file was ported in #52.
  • Loading branch information
eric-wieser authored and fgdorais committed Jul 25, 2023
1 parent eb0b3aa commit e8ad043
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion bors.toml
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
status = ["Build", "Lint style", "Check all files imported"]
use_squash_merge = true
timeout_sec = 28800
block_labels = ["not-ready-to-merge", "WIP", "blocked-by-other-PR", "merge-conflict"]
block_labels = ["not-ready-to-merge", "WIP", "blocked-by-other-PR", "merge-conflict", "awaiting-CI"]
delete_merged_branches = true
update_base_for_deletes = true
cut_body_after = "---"

0 comments on commit e8ad043

Please sign in to comment.