From 4e58b428e99e7f73db470663994b2d033e382274 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 15 Feb 2024 17:42:57 +0100 Subject: [PATCH] doc: add Kyle Miller as delaborator code owner --- CODEOWNERS | 1 + 1 file changed, 1 insertion(+) diff --git a/CODEOWNERS b/CODEOWNERS index 7ef90703b0..846025a850 100644 --- a/CODEOWNERS +++ b/CODEOWNERS @@ -17,6 +17,7 @@ /src/Lean/Meta/Tactic/ @leodemoura /src/Lean/Parser/ @Kha /src/Lean/PrettyPrinter/ @Kha +/src/Lean/PrettyPrinter/Delaborator/ @kmill /src/Lean/Server/ @mhuisi /src/Lean/Widget/ @Vtec234 /src/runtime/io.cpp @joehendrix