From 204b408df7b11cdd09cef04ea1d03d8fc5d1d18e Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 19 Feb 2024 17:30:21 +0100 Subject: [PATCH] chore: remove noisy root code owners --- CODEOWNERS | 1 - 1 file changed, 1 deletion(-) diff --git a/CODEOWNERS b/CODEOWNERS index 846025a850..2c9402d71c 100644 --- a/CODEOWNERS +++ b/CODEOWNERS @@ -6,7 +6,6 @@ /.github/ @Kha @semorrison /RELEASES.md @semorrison -/src/ @leodemoura @Kha /src/Init/IO.lean @joehendrix /src/kernel/ @leodemoura /src/lake/ @tydeu