Remove code owners from low-risk files
This leaves an empty list, the behaviour of which isn't documented, but experiments show github does not consider anyone to be a code owner for those files and does not automatically request any reviews for them.
This commit is contained in:
parent
8f8052a5b0
commit
39323e00a2
10
CODEOWNERS
10
CODEOWNERS
|
@ -48,12 +48,12 @@
|
||||||
|
|
||||||
# These files change frequently and changes are low-risk
|
# These files change frequently and changes are low-risk
|
||||||
|
|
||||||
/src/util/irep_ids.def @diffblue/cbmc-developers
|
/src/util/irep_ids.def
|
||||||
|
|
||||||
/unit/ @diffblue/cbmc-developers
|
/unit/
|
||||||
/regression/ @diffblue/cbmc-developers
|
/regression/
|
||||||
/jbmc/unit/ @diffblue/cbmc-developers
|
/jbmc/unit/
|
||||||
/jbmc/regression/ @diffblue/cbmc-developers
|
/jbmc/regression/
|
||||||
|
|
||||||
/scripts/ @diffblue/devops @thk123 @forejtv @peterschrammel
|
/scripts/ @diffblue/devops @thk123 @forejtv @peterschrammel
|
||||||
/.travis.yml @diffblue/devops @thk123 @forejtv @peterschrammel
|
/.travis.yml @diffblue/devops @thk123 @forejtv @peterschrammel
|
||||||
|
|
Loading…
Reference in New Issue