aboutsummaryrefslogtreecommitdiffhomepage
path: root/.github/CODEOWNERS
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-03-26 10:41:02 +0200
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-03-26 10:41:02 +0200
commit092c35f88566e11562a1c10e22e551c2d635439b (patch)
tree8a1ffc1dd5b78535a574cb23f25fd40a3a38bcab /.github/CODEOWNERS
parentd8603ba5bc093a479bc30df580f4f25709681c16 (diff)
Add Michael Soegtrop as a code owner for Windows build scripts.
Diffstat (limited to '.github/CODEOWNERS')
-rw-r--r--.github/CODEOWNERS3
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 ##########