From 119f685cda330fc85bb07f61b98a62d367a22c51 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sun, 8 Aug 2021 18:39:28 +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 10b272b3d9..6e608e3779 100644 --- a/doc/setup.md +++ b/doc/setup.md @@ -39,7 +39,7 @@ It has been tested on Windows by installing these tools using [MSYS2](https://ww ### Editing -Lean implements the [Language Server Protocol](https://microsoft.github.io/language-server-protocol/) that can be used for interactive development in [Emacs](https://github.com/leanprover/lean4/tree/master/lean4-mode/README.md), [VS Code](https://github.com/mhuisi/vscode-lean4), and possibly other editors. +Lean implements the [Language Server Protocol](https://microsoft.github.io/language-server-protocol/) that can be used for interactive development in [Emacs](https://github.com/leanprover/lean4/tree/master/lean4-mode/README.md), [VS Code](https://github.com/leanprover-community/vscode-lean4), and possibly other editors. Changes must be saved to be visible in other files, which must then be invalidated using an editor command (see links above).