aboutsummaryrefslogtreecommitdiffhomepage
path: root/.github/CODEOWNERS
diff options
context:
space:
mode:
Diffstat (limited to '.github/CODEOWNERS')
-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 ##########