diff options
| author | Maxime Dénès | 2018-04-30 09:34:40 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-04-30 09:34:40 +0200 |
| commit | 86cfc249dc7cc95d772ed91663491ee8b37c1431 (patch) | |
| tree | cab160ea69e29c70b40956046a7af37fd1214ae5 | |
| parent | 8c3d9eb165b456fc83753624efe6708832e9b52f (diff) | |
| parent | 8d9739f20a4fec2194fda525ed2cca8d4be297ed (diff) | |
Merge PR #7355: [owners] Makefile.ci belongs to the CI category.
| -rw-r--r-- | .github/CODEOWNERS | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 7f3ee5c37d..329697ca4b 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -302,6 +302,9 @@ /dev/build/windows @MSoegtropIMC # Secondary maintainer @maximedenes +# This file belongs to CI +Makefile.ci @ejgallego +# Secondary maintainer @SkySkimmer ########## Developer tools ########## |