max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: fix link

Browse source
This commit is contained in:
Sebastian Ullrich 2021-08-08 18:39:28 +02:00 • committed by GitHub
parent 40274e487f
commit 119f685cda
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
doc/setup.md
View file

@ -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).