labels: no CI label for OWNERS changes
We can use the same "hack" as in labeler-no-sync.yml, because OWNERS is the only file without extension in that directory structure. This makes it easier to search for CI related PRs via label.
This commit is contained in:
2
.github/labeler.yml
vendored
2
.github/labeler.yml
vendored
@@ -39,7 +39,7 @@
|
|||||||
- changed-files:
|
- changed-files:
|
||||||
- any-glob-to-any-file:
|
- any-glob-to-any-file:
|
||||||
- .github/**/*
|
- .github/**/*
|
||||||
- ci/**/*
|
- ci/**/*.*
|
||||||
|
|
||||||
"6.topic: coq":
|
"6.topic: coq":
|
||||||
- any:
|
- any:
|
||||||
|
|||||||
Reference in New Issue
Block a user