From af98453ba4aea9a039d7e790028f1e4a70928862 Mon Sep 17 00:00:00 2001 From: JadAbouHawili Date: Sat, 11 Apr 2026 17:07:46 +0300 Subject: [PATCH 1/2] Update PR guidelines to refer to pull request conventions --- templates/contribute/index.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/templates/contribute/index.md b/templates/contribute/index.md index c8474031e..a53242e9b 100644 --- a/templates/contribute/index.md +++ b/templates/contribute/index.md @@ -133,7 +133,7 @@ Once you're happy with your local changes, it's time to make a pull request. This helps you get feedback as you go along, and it is much easier to review. This is especially important for new contributors as it prevents wasted effort. -* The title and description of the PR should follow our [commit conventions](commit.html). +* The title and description of the PR should follow our [pull request 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: From d3140fa87034d3617a14edebef6a368c5d816f9c Mon Sep 17 00:00:00 2001 From: JadAbouHawili Date: Sat, 11 Apr 2026 17:09:53 +0300 Subject: [PATCH 2/2] Update commit conventions to pull request conventions --- data/menus.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/data/menus.yaml b/data/menus.yaml index 9c7bb3dcc..f436ff752 100644 --- a/data/menus.yaml +++ b/data/menus.yaml @@ -54,7 +54,7 @@ - Naming conventions: contribute/naming.html - Code style guideline: contribute/style.html - Documentation style: contribute/doc.html - - Commit conventions: contribute/commit.html + - Pull Request conventions: contribute/commit.html - Pull request review guide: contribute/pr-review.html - Contribution statistics: mathlib_stats.html - Tags and branches: contribute/tags_and_branches.html