From df6626f06b8f5ecba550bfa24523211c4ebb49b1 Mon Sep 17 00:00:00 2001
From: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>
Date: Mon, 30 Oct 2023 00:58:25 +0100
Subject: [PATCH] doc: fix a link in development documentation #2780

---
 doc/dev/index.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/dev/index.md b/doc/dev/index.md
index e6e08f13b5..1832dea5d3 100644
--- a/doc/dev/index.md
+++ b/doc/dev/index.md
@@ -1,6 +1,6 @@
 # Development Workflow
 
-If you want to make changes to Lean itself, start by [building Lean](../make/index.html) from a clean checkout to make sure that everything is set up correctly.
+If you want to make changes to Lean itself, start by [building Lean](../make/index.md) from a clean checkout to make sure that everything is set up correctly.
 After that, read on below to find out how to set up your editor for changing the Lean source code, followed by further sections of the development manual where applicable such as on the [test suite](testing.md) and [commit convention](commit_convention.md).
 
 If you are planning to make any changes that may affect the compilation of Lean itself, e.g. changes to the parser, elaborator, or compiler, you should first read about the [bootstrapping pipeline](bootstrap.md).