chore: update code owners
This commit is contained in:
parent
706a4cfd73
commit
22a581f38d
1 changed files with 0 additions and 2 deletions
|
|
@ -6,7 +6,6 @@
|
|||
|
||||
/.github/ @Kha @semorrison
|
||||
/RELEASES.md @semorrison
|
||||
/src/Init/IO.lean @joehendrix
|
||||
/src/kernel/ @leodemoura
|
||||
/src/lake/ @tydeu
|
||||
/src/Lean/Compiler/ @leodemoura
|
||||
|
|
@ -20,7 +19,6 @@
|
|||
/src/Lean/PrettyPrinter/Delaborator/ @kmill
|
||||
/src/Lean/Server/ @mhuisi
|
||||
/src/Lean/Widget/ @Vtec234
|
||||
/src/runtime/io.cpp @joehendrix
|
||||
/src/Init/Data/ @semorrison
|
||||
/src/Init/Data/Array/Lemmas.lean @digama0
|
||||
/src/Init/Data/List/Lemmas.lean @digama0
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue