Skip to content

Commit

Permalink
chore: adjust CODEOWNERS (#6327)
Browse files Browse the repository at this point in the history
Remove some noise from my assignments
  • Loading branch information
Kha authored Dec 10, 2024
1 parent 8a3a806 commit a805946
Showing 1 changed file with 2 additions and 4 deletions.
6 changes: 2 additions & 4 deletions CODEOWNERS
Validating CODEOWNERS rules …
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down

0 comments on commit a805946

Please sign in to comment.