chore: remove noisy root code owners

This commit is contained in:
Sebastian Ullrich
2024-02-19 17:30:21 +01:00
committed by GitHub
parent 7545b85512
commit 204b408df7

View File

@@ -6,7 +6,6 @@
/.github/ @Kha @semorrison
/RELEASES.md @semorrison
/src/ @leodemoura @Kha
/src/Init/IO.lean @joehendrix
/src/kernel/ @leodemoura
/src/lake/ @tydeu