From a805946466e2ee13246e0fd1790d0c435dfd63dd Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 10 Dec 2024 09:37:20 +0100 Subject: [PATCH] chore: adjust CODEOWNERS (#6327) Remove some noise from my assignments --- CODEOWNERS | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/CODEOWNERS b/CODEOWNERS index 9695c7371d..05c47fe217 100644 --- a/CODEOWNERS +++ b/CODEOWNERS @@ -4,7 +4,7 @@ # Listed persons will automatically be asked by GitHub to review a PR touching these paths. # If multiple names are listed, a review by any of them is considered sufficient by default. -/.github/ @Kha @kim-em +/.github/ @kim-em /RELEASES.md @kim-em /src/kernel/ @leodemoura /src/lake/ @tydeu @@ -14,9 +14,7 @@ /src/Lean/Elab/Tactic/ @kim-em /src/Lean/Language/ @Kha /src/Lean/Meta/Tactic/ @leodemoura -/src/Lean/Parser/ @Kha -/src/Lean/PrettyPrinter/ @Kha -/src/Lean/PrettyPrinter/Delaborator/ @kmill +/src/Lean/PrettyPrinter/ @kmill /src/Lean/Server/ @mhuisi /src/Lean/Widget/ @Vtec234 /src/Init/Data/ @kim-em