aboutsummaryrefslogtreecommitdiffhomepage
path: root/.github
diff options
context:
space:
mode:
authorGravatar Michael Soegtrop <michael.soegtrop@intel.com>2018-06-15 18:57:00 +0200
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-06-25 16:37:02 +0200
commitcb885e8c70a75043ff89e117c29cbb5dc22ff16f (patch)
tree9b9d84ef9f0b7151c33bb889493679e01aad92d6 /.github
parent915452f9a73d25e45131edb08531c29a79ab7020 (diff)
Fix for issue 7707: include Ltac2 and Equations in Windows build
On the way I also fixed some minor issues with calling MakeCoq_MinGW from cygwin.
Diffstat (limited to '.github')
-rw-r--r--.github/CODEOWNERS3
1 files changed, 3 insertions, 0 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS
index 3a762b42a..0278df72f 100644
--- a/.github/CODEOWNERS
+++ b/.github/CODEOWNERS
@@ -339,6 +339,9 @@
/dev/build/windows @MSoegtropIMC
# Secondary maintainer @maximedenes
+/dev/build/plugin-versions @MSoegtropIMC
+# Secondary maintainer @maximedenes
+
# This file belongs to CI
/Makefile.ci @ejgallego
# Secondary maintainer @SkySkimmer