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 `---`.