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

doc(msvc): add instructions on how to get Intellisense working

Browse source
This commit is contained in:
Nuno Lopes 2018-01-28 15:56:56 +00:00 • committed by Leonardo de Moura
parent 46cfd33a1b
commit 8019914ad4
2 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
.gitignore vendored
View file

@ -21,3 +21,4 @@ settings.json
/*.nix
/library/init/version.lean
CMakeSettings.json
CppProperties.json

6
doc/make/msvc.md
View file

@ -29,6 +29,12 @@ In each of the targets, add the following snippet (i.e., after every
```
## Enable Intellisense
In Visual Studio, press Ctrl+Q and type `CppProperties.json` and press Enter.
Ensure `includePath` variables include `C:\\path\\to\\lean\\src`.
## Build Lean
Press F7.