From 161ef7a67c8eecdbef6815751ebe1dd02d9bd300 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Mon, 1 Aug 2022 13:01:56 +0200 Subject: [PATCH] doc: fix link --- doc/setup.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/setup.md b/doc/setup.md index 5be695fe5a..d19245b8ab 100644 --- a/doc/setup.md +++ b/doc/setup.md @@ -125,7 +125,7 @@ If you don't want to or cannot start the pinned editor from Nix, e.g. because yo $ nix build .#lean-dev -o result-lean-dev ``` The resulting `./result-lean-dev/bin/lean` script essentially runs `nix run .#lean` in the current project's root directory when you open a Lean file or use the "refresh dependencies" command such that the correct Lean version for that project is executed. -This includes selecting the correct stage of Lean (which it will compile on the fly, though without progress output) if you are [working on Lean itself](../make/nix.md#editor-integration). +This includes selecting the correct stage of Lean (which it will compile on the fly, though without progress output) if you are [working on Lean itself](./make/nix.md#editor-integration). Package dependencies can be added as further input flakes and passed to the `deps` list of `buildLeanPackage`. Example: