From d2b82bf5638dc60ae2d552d64c2a2a532547239f Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 23 Dec 2020 19:36:27 +0100 Subject: [PATCH] doc: LSP setup using Nix --- doc/make/nix.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/doc/make/nix.md b/doc/make/nix.md index 2909607528..4d91819b91 100644 --- a/doc/make/nix.md +++ b/doc/make/nix.md @@ -70,6 +70,8 @@ Starting a known-good (pinned) version of Emacs from the Lean shell with `lean4- ```bash nix run .#emacs-dev ``` +After adding `src/` as an LSP workspace using `lsp-workspace-folder-add`, it should automatically fall back to using stage 0 in there. + If you've already installed lean4-mode manually, you might need to first deactivate that. `elan` can be left as is on the other hand. Arguments can be passed as well: