diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 3054467f53d..a787f902745 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -33,4 +33,6 @@ src/js_of_ocaml* @hhugo editor_integration/emacs/* @Chris00 -doc/* @emillon @rgrinberg \ No newline at end of file +doc/* @emillon @rgrinberg + +src/coq_* @ejgallego