From 86364fdc220b9a170b7593400ef2da6e47cd142a Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 21 Mar 2018 16:43:09 +0100 Subject: Owners for developer tools --- .github/CODEOWNERS | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) (limited to '.github') diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 3c0603d8e..fb4d07333 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -293,3 +293,24 @@ /META.coq @ejgallego # Secondary maintainer @letouzey + + +########## Developer tools ########## + +/dev/tools/backport-pr.sh @Zimmi48 +# Secondary maintainer @maximedenes + +/dev/tools/change-header @herbelin + +/dev/tools/check-eof-newline.sh @SkySkimmer + +/dev/tools/coqdev.el @SkySkimmer + +/dev/tools/github-check-prs.py @SkySkimmer + +/dev/tools/merge-pr.sh @maximedenes +# Secondary maintainer @gares + +/dev/tools/pre-commit @SkySkimmer + +/dev/tools/sudo-apt-get-update @JasonGross -- cgit v1.2.3