aboutsummaryrefslogtreecommitdiffhomepage
path: root/.github
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-05-08 08:25:33 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-05-08 08:25:33 +0200
commite31933a321195df1b076a044d936fd2d9190444d (patch)
tree9accd5c50d9d315a9566e6a9fe8320fc31c0c2a6 /.github
parent6c8b00e47334f60f200256d45a5542fa80ce4b12 (diff)
Try to fix CODEOWNERS
Diffstat (limited to '.github')
-rw-r--r--.github/CODEOWNERS12
1 files changed, 6 insertions, 6 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS
index afa95420c..ab9725c96 100644
--- a/.github/CODEOWNERS
+++ b/.github/CODEOWNERS
@@ -71,9 +71,9 @@
/engine/ @ppedrot
# Secondary maintainer @aspiwack
-/engine/universes.ml{,i} @SkySkimmer
-/engine/univops.ml{,i} @SkySkimmer
-/engine/uState.ml{,i} @SkySkimmer
+/engine/universes.* @SkySkimmer
+/engine/univops.* @SkySkimmer
+/engine/uState.* @SkySkimmer
# Secondary maintainer @mattam82
########## Grammar macros ##########
@@ -99,9 +99,9 @@
/kernel/byterun/ @maximedenes
# Secondary maintainer @silene
-/kernel/sorts.ml{,i} @SkySkimmer
-/kernel/uGraph.ml{,i} @SkySkimmer
-/kernel/univ.ml{,i} @SkySkimmer
+/kernel/sorts.* @SkySkimmer
+/kernel/uGraph.* @SkySkimmer
+/kernel/univ.* @SkySkimmer
# Secondary maintainer @mattam82
########## Library ##########