08c4f81596
Also: set the build and install directories to the source directory because the build system unfortunately expects the `src_ext` directory to be under the current working directory when building the bundled third-party libraries, even when the configure script is run from another directory. @scemama pointed out that 'make' just calls 'dune' which is already parallel, so make itself should not have more than one job. opam@:2.1 need 'make lib-ext' for cmdliner, above it's obsolete. Co-authored-by: Bernhard Kaindl <bernhard.kaindl@cloud.com> |
||
|---|---|---|
| .. | ||
| gpg | ||
| gpg.mock | ||
| repos | ||