diff --git a/doc/dev/index.md b/doc/dev/index.md index 7b352889d5..a3dd60b0b8 100644 --- a/doc/dev/index.md +++ b/doc/dev/index.md @@ -8,7 +8,7 @@ You should not edit the `stage0` directory except using the commands described i ## Development Setup -You can use any of the [supported editors](../setup.md) for editing the Lean source code. +You can use any of the [supported editors](https://lean-lang.org/install/manual/) for editing the Lean source code. Please see below for specific instructions for VS Code. ### Dev setup using elan diff --git a/doc/make/index.md b/doc/make/index.md index 93c22e69c6..7dd4f5dbd1 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](../dev/index.md). -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. +We strongly suggest that new users instead follow the [Installation Instructions](https://lean-lang.org/install/) 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 ------------