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

doc: wording

Browse source
This commit is contained in:
Sebastian Ullrich 2020-08-25 16:12:19 +02:00 • committed by GitHub
parent 21d176c1ea
commit 589afc4095
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
doc/make/msys2.md
View file

@ -4,17 +4,17 @@
Lean for Windows
----------------
A native Lean binary for Windows can be generated using [msys2].
A native Lean binary for Windows can be generated using [MSYS2][msys2].
It is easy to install all dependencies, it produces native
64/32-binaries, and supports a C++14 compiler.
## Installing dependencies
[The official webpage of msys2][msys2] provides one-click installers.
Once installed it, you should run the "MSYS2 MinGW 64-bit shell" from the start menu.
[The official webpage of MSYS2][msys2] provides one-click installers.
Once installed, you should run the "MSYS2 MinGW 64-bit shell" from the start menu.
Do not run "MSYS2 MSYS" instead!
MSYS2 MinGW has a package management system, [pacman][pacman], which is used in Arch Linux.
MSYS2 has a package management system, [pacman][pacman], which is used in Arch Linux.
Here are the commands to install all dependencies needed to compile Lean on your machine.
@ -22,7 +22,7 @@ Here are the commands to install all dependencies needed to compile Lean on your
pacman -S make python mingw-w64-x86_64-cmake mingw-w64-x86_64-ccache mingw-w64-x86_64-clang git
```
Then follow the [generic build instructions](index.md) in the [msys2] shell, using
Then follow the [generic build instructions](index.md) in the MSYS2 MinGW shell, using
`cmake ../.. -G "Unix Makefiles"` instead of `cmake ../..`. This ensures that cmake will call `sh` instead
of `cmd.exe` for script tasks.