From 54a50e9fa81140a62a5d10e092c238df52d5c585 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Thu, 30 Sep 2021 11:27:40 +0100 Subject: [PATCH] Change ownership of `src/config.inc` file to @diffblue/diffblue-opensource. 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). --- CODEOWNERS | 1 + 1 file changed, 1 insertion(+) diff --git a/CODEOWNERS b/CODEOWNERS index 9513faf65e6..0d1c241a717 100644 --- 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