From 2712385b3be959b5f4a946603d835971ef945f4b Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Fri, 22 May 2026 23:12:53 +0200 Subject: [PATCH] chore(how-to-contribute): remove portion about (re)moving declarations from the PR description. This clogs up the template and has not been used in practice at all. In the future, semantic diffing will provide this information. --- templates/contribute/how-to-contribute.md | 11 ----------- 1 file changed, 11 deletions(-) diff --git a/templates/contribute/how-to-contribute.md b/templates/contribute/how-to-contribute.md index ed8cc8558..8595d311d 100644 --- a/templates/contribute/how-to-contribute.md +++ b/templates/contribute/how-to-contribute.md @@ -76,17 +76,6 @@ Once you're happy with your local changes, it's time to make a pull request. * The title and description of the PR should follow our [commit conventions](commit.html). -* If you are moving or deleting declarations, please include these lines at the bottom of the commit message -(that is, before the `---`) using the following format: - -Moves: -- Vector.* -> Mathlib.Vector.* -- ... - -Deletions: -- Nat.bit1_add_bit1 -- ... - Any other comments you want to keep out of the PR commit should go below the `---`.