labels: no CI label for OWNERS changes (#406133)
This commit is contained in:
+1
-1
@@ -39,7 +39,7 @@
|
||||
- changed-files:
|
||||
- any-glob-to-any-file:
|
||||
- .github/**/*
|
||||
- ci/**/*
|
||||
- ci/**/*.*
|
||||
|
||||
"6.topic: coq":
|
||||
- any:
|
||||
|
||||
Reference in New Issue
Block a user