From 2877196656fb67bdeeea3d26eb874963cf188fa3 Mon Sep 17 00:00:00 2001 From: Dax Fohl Date: Tue, 2 Sep 2025 05:45:04 -0700 Subject: [PATCH] doc: fix broken "quickstart" and "supported editors" link (#8785) The "supported editors" link in https://github.com/leanprover/lean4/blob/master/doc/dev/index.md is broken, as `setup.md` no longer exists in the repo. This PR changes the link to point to the live Lean docs setup page at https://docs.lean-lang.org/lean4/doc/setup.html#editing. A similar fix for quickstart is included. --------- Co-authored-by: Sebastian Ullrich --- doc/dev/index.md | 2 +- doc/make/index.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) 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 ------------