From b053679d6dce4dd29ba773e37d4ba5cbe65232bb Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 9 Nov 2021 09:55:11 +0100 Subject: [PATCH] doc: fix a few links --- CONTRIBUTING.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index d80da1d325..4abe84c09e 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -50,8 +50,8 @@ We don't want to waste your time by you implementing a feature and then us not b ## How to Contribute -* Always follow the [commit convention](https://leanprover.github.io/lean4/doc/commit_convention.html). +* Always follow the [commit convention](https://leanprover.github.io/lean4/doc/dev/commit_convention.html). * Follow the style of the surrounding code. When in doubt, look at other files using the particular syntax as well. * Make sure your code is documented. * New features or bug fixes should come with appropriate tests. -* Ensure all tests work before submitting a PR; see [Development Setup](https://leanprover.github.io/lean4/doc/make/index.html#development-setup) and [Fixing Tests](https://leanprover.github.io/lean4/doc/fixing_tests.html). +* Ensure all tests work before submitting a PR; see [Development Setup](https://leanprover.github.io/lean4/doc/make/index.html#development-setup) and [Fixing Tests](https://leanprover.github.io/lean4/doc/dev/fixing_tests.html).