diff options
| author | Emilio Jesus Gallego Arias | 2021-03-29 18:18:06 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2021-04-01 17:09:58 +0200 |
| commit | 7f629fc3270a1ecfa6b37fc2d85fc3a8a751af6e (patch) | |
| tree | 79a726c78b423f4eac4f681d92b818db819a24b7 /Makefile.dune | |
| parent | 05957f023e0c917f572e652f56d92efb67a824fa (diff) | |
[doc] [dune] Some tweaks from #13617
Tweaks to docs that are independent / unrelated to that PR.
Diffstat (limited to 'Makefile.dune')
| -rw-r--r-- | Makefile.dune | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.dune b/Makefile.dune index c338405f2c..1313ef5eac 100644 --- a/Makefile.dune +++ b/Makefile.dune @@ -18,7 +18,7 @@ help: @echo " - world: build all public binaries and libraries" @echo " - watch: build all public binaries and libraries [continuous build]" @echo " - check: build all ML files as fast as possible" - @echo " - test-suite: run Coq's test suite" + @echo " - test-suite: run Coq's test suite [env NJOBS=N to set job parallelism]" @echo "" @echo " Note: running ./configure is not recommended," @echo " see dev/doc/build-system.dune.md for more info" |