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