From a6f63cfb4159fe28b7a4d6a6a13cc8c799fca78c Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 5 Nov 2024 11:20:38 +0100 Subject: [PATCH] fix links --- doc/make/index.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/make/index.md b/doc/make/index.md index 1bf663760ce8..40cd1e8ee833 100644 --- a/doc/make/index.md +++ b/doc/make/index.md @@ -1,6 +1,6 @@ -These are instructions to set up a working development environment for those who wish to make changes to Lean itself. It is part of the [Development Guide](doc/dev/index.md). +These are instructions to set up a working development environment for those who wish to make changes to Lean itself. It is part of the [Development Guide](../dev/index.md). -We strongly suggest that new users instead follow the [Quickstart](doc/quickstart.md) to get started using Lean, since this sets up an environment that can automatically manage multiple Lean toolchain versions, which is necessary when working within the Lean ecosystem. +We strongly suggest that new users instead follow the [Quickstart](../quickstart.md) to get started using Lean, since this sets up an environment that can automatically manage multiple Lean toolchain versions, which is necessary when working within the Lean ecosystem. Requirements ------------