diff options
| -rw-r--r-- | .github/CODEOWNERS | 17 |
1 files changed, 7 insertions, 10 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 512a9c99eb..13e6029255 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -274,16 +274,6 @@ /theories/Vectors/ @herbelin -########## Dune ########## - -/.ocamlinit @ejgallego -/Makefile.dune @ejgallego -/tools/coq_dune* @ejgallego -/dune* @ejgallego -/coq.opam @ejgallego -/ide/coqide.opam @ejgallego -# Secondary maintainer @Zimmi48 - ########## Tools ########## /tools/coqdoc/ @silene @@ -358,3 +348,10 @@ /dev/tools/update-compat.py @JasonGross /test-suite/tools/update-compat/ @JasonGross # Secondary maintainer @Zimmi48 + +########## Dune ########## + +/.ocamlinit @ejgallego +*dune* @ejgallego +*.opam @ejgallego +# Secondary maintainer @Zimmi48 |