From 9bf0f5116b69536d6c2471510f64194791afed69 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 20 Nov 2023 09:30:18 +0100 Subject: [PATCH] chore: more code owners --- CODEOWNERS | 1 + 1 file changed, 1 insertion(+) diff --git a/CODEOWNERS b/CODEOWNERS index 3a8f591328..e9aefd6deb 100644 --- a/CODEOWNERS +++ b/CODEOWNERS @@ -12,6 +12,7 @@ /src/lake/ @tydeu /src/Lean/Compiler/ @leodemoura /src/Lean/Data/Lsp/ @mhuisi +/src/Lean/Elab/Deriving/ @semorrison /src/Lean/Elab/Tactic/ @semorrison /src/Lean/Meta/Tactic/ @leodemoura /src/Lean/Parser/ @Kha