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

doc: advise using Developer Mode on Windows

Browse source
This commit is contained in:
Sebastian Ullrich 2021-11-16 11:59:26 +01:00
parent 44f9edff87
commit dbdb92a411
1 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
doc/make/msys2.md
View file

@ -9,6 +9,12 @@ It is easy to install all dependencies, it produces native
An alternative to MSYS2 is to use [Lean in Windows WSL](wsl.md).
While not necessary for pure building, you should first activate [Developer
Mode](https://docs.microsoft.com/en-us/windows/apps/get-started/enable-your-device-for-development)
(Settings > Update & Security > For developers > Developer Mode),
which will allow Lean to create symlinks that e.g. enable go-to-definition in
the stdlib.
## Installing dependencies
[The official webpage of MSYS2][msys2] provides one-click installers.