Change ownership of src/config.inc file to @diffblue/diffblue-opensource.

NlightNFotis · NlightNFotis · commit 54a50e9fa811 · 2021-09-30T11:27:40.000+01:00
This is a minor change to allow for faster releases, by requiring less people
to sign off a release PR (it is now okay if it's signed off by a member of the
team maintaining CBMC in diffblue - the people that have been handling releases
in any case).
diff --git a/CODEOWNERS b/CODEOWNERS
@@ -75,3 +75,4 @@ CMakeLists.txt @diffblue/diffblue-opensource
 
 # CI pipeline is the responsibility of the Open Source maintenance team at Diffblue.
 /.github/ @diffblue/diffblue-opensource
+src/config.inc @diffblue/diffblue-opensource

Original file line number	Diff line number	Diff line change
`@@ -75,3 +75,4 @@ CMakeLists.txt @diffblue/diffblue-opensource`
`75`	`75`
`76`	`76`	`# CI pipeline is the responsibility of the Open Source maintenance team at Diffblue.`
`77`	`77`	`/.github/ @diffblue/diffblue-opensource`
	`78`	`+src/config.inc @diffblue/diffblue-opensource`