diff options
| author | Théo Zimmermann | 2018-05-02 15:02:34 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-05-02 15:02:34 +0200 |
| commit | 48ec42bb91b8c0fb4d5930e62e29a408de594482 (patch) | |
| tree | e2a1328481ebaa3af55a07d1d112761194b6aaef /.github | |
| parent | 6062f9f6a3770f967b6d540756063a3992131a6c (diff) | |
| parent | 6cbd1b0cbb5693e2188463a293054ce1169c7cbe (diff) | |
Merge PR #7403: Makefile doc owners
Diffstat (limited to '.github')
| -rw-r--r-- | .github/CODEOWNERS | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 329697ca4b..74bbda5533 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -303,9 +303,12 @@ # Secondary maintainer @maximedenes # This file belongs to CI -Makefile.ci @ejgallego +/Makefile.ci @ejgallego # Secondary maintainer @SkySkimmer +/Makefile.doc @maximedenes +# Secondary maintainer @silene + ########## Developer tools ########## /dev/tools/backport-pr.sh @Zimmi48 |