diff options
| author | coqbot-app[bot] | 2021-04-01 13:22:01 +0000 |
|---|---|---|
| committer | GitHub | 2021-04-01 13:22:01 +0000 |
| commit | 7db6dfcf8d4f1023b17ee4d73e22f79f73983162 (patch) | |
| tree | 4af0d89379a6a5e44f4e72011315aa98252501c7 /doc/sphinx/practical-tools/utilities.rst | |
| parent | 1a64b1560ce88855a76e2faa14cec2864de2f37c (diff) | |
| parent | 7dba32f3204b85b0abf39161c7c8b7db4ce27247 (diff) | |
Merge PR #14018: [doc] [coq_makefile] Document that -j N is broken for OCaml < 4.07.0
Reviewed-by: JasonGross
Ack-by: jfehrle
Diffstat (limited to 'doc/sphinx/practical-tools/utilities.rst')
| -rw-r--r-- | doc/sphinx/practical-tools/utilities.rst | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 5d36ec3cf9..49c2c6b785 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -515,6 +515,11 @@ To build, say, two targets foo.vo and bar.vo in parallel one can use + ``-extra-phony`` and ``-extra`` are deprecated. To provide additional target (``.PHONY`` or not) please use ``CoqMakefile.local``. +.. note:: + + Due to limitations with the compilation chain, makefiles generated + by ``coq_makefile`` won't correctly compile OCaml plugins with OCaml + < 4.07.0 when using more than one job (``-j N`` for ``N > 1``). Precompiling for ``native_compute`` +++++++++++++++++++++++++++++++++++ |