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

doc: fix ctest advice

Browse source
This commit is contained in:
Sebastian Ullrich 2020-12-29 22:52:27 +01:00 • committed by Leonardo de Moura
parent 227393ef58
commit b0f1bfb580
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/make/index.md
View file

@ -137,7 +137,7 @@ Development Setup
-----------------
After building a stage, you can invoke `make -C stageN test` (or, even better,
`make -C stageN ARGS=-j` to make `ctest` parallel) to run the Lean test suite.
`make -C stageN test ARGS=-jN` to make `ctest` parallel) to run the Lean test suite.
`make test` without `-C` defaults to stage1. While the Lean tests will
automatically use that stage's corresponding Lean executables, for running tests
or compiling Lean programs manually, you need to put them into your `PATH`