aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-04-11 10:04:47 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-04-11 10:05:55 +0200
commitfde6edf6490faa51140f267c677b8417a08daf9f (patch)
tree4da954ded38630c234f472f8d58f3165be013ff7
parentccf5c0879e3341ebfc8d3d00d35cc10b8b32a9e4 (diff)
Add myself as the primary maintainer of the warnings system
-rw-r--r--.github/CODEOWNERS3
1 files changed, 3 insertions, 0 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS
index f344c5cf5..2d8fc791b 100644
--- a/.github/CODEOWNERS
+++ b/.github/CODEOWNERS
@@ -60,6 +60,9 @@
/lib/ @ejgallego
# Secondary maintainer @ppedrot
+/lib/cWarnings.* @maximedenes
+# Secondary maintainer @ejgallego
+
########## Proof engine ##########
/engine/ @ppedrot