diff options
| author | Théo Zimmermann | 2018-03-22 18:05:22 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2018-03-22 18:05:22 +0100 |
| commit | cbd6e207006b0aca56d4b2400c5b0b2e8e88c49a (patch) | |
| tree | 50fed71c0765739fa84dbeb2e97a2fad9330e8cb | |
| parent | d275cbc0980ecca00c6a8e0ed172df67eef3d8f4 (diff) | |
| parent | 86364fdc220b9a170b7593400ef2da6e47cd142a (diff) | |
Merge PR #7031: Owners for developer tools
| -rw-r--r-- | .github/CODEOWNERS | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 3c0603d8e0..fb4d073337 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 |