diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-03-26 10:41:02 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-03-26 10:41:02 +0200 |
| commit | 092c35f88566e11562a1c10e22e551c2d635439b (patch) | |
| tree | 8a1ffc1dd5b78535a574cb23f25fd40a3a38bcab /.github | |
| parent | d8603ba5bc093a479bc30df580f4f25709681c16 (diff) | |
Add Michael Soegtrop as a code owner for Windows build scripts.
Diffstat (limited to '.github')
| -rw-r--r-- | .github/CODEOWNERS | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index ee291aebb..d33a0c59f 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -294,6 +294,9 @@ /META.coq @ejgallego # Secondary maintainer @letouzey +/dev/build/windows @MSoegtropIMC +# Secondary maintainer @maximedenes + ########## Developer tools ########## |