doc: code owners (#2875)

This commit is contained in:
Sebastian Ullrich 2023-11-15 18:21:23 +01:00 committed by GitHub
parent 7fb7b5c5cb
commit 7cc2c9f1c9
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23

18
CODEOWNERS Normal file
View file

@ -0,0 +1,18 @@
# Code Owners
#
# Documents responsible people per component.
# 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 @semorrison
/RELEASES.md @semorrison
/src/ @leodemoura @Kha
/src/Init/IO.lean @joehendrix
/src/kernel/ @leodemoura
/src/lake/ @tydeu
/src/Lean/Compiler/ @leodemoura
/src/Lean/Elab/Tactic/ @semorrison
/src/Lean/Meta/Tactic/ @leodemoura
/src/Lean/Parser/ @Kha
/src/Lean/PrettyPrinter/ @Kha
/src/Lean/Server/ @mhuisi