diff options
| author | Maxime Dénès | 2018-10-01 15:03:49 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-10-01 15:03:49 +0200 |
| commit | c0c3d7f8953323cd5613b0f6c3217f1451a5a060 (patch) | |
| tree | a2a358716768e30d3555e5ac979567d8fbb58c38 /dev | |
| parent | aff4c089548c4e77b93a5676fe82abf93189d6ce (diff) | |
| parent | f0c7587ea53b855ca58ce73d3e25f7e81215a722 (diff) | |
Merge PR #8579: [dune] [merlin] Fix some usability issues.
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/doc/build-system.dune.md | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index 85aaf317ef..36d5e5841b 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -3,6 +3,23 @@ Dune-based build system. If you want to enhance the build system itself (or are curious about its implementation details), see build-system.dev.txt, and in particular its initial HISTORY section. +Quick Start +=========== + +You need Dune >= 1.2.1 ; just type `dune build` to build the base Coq +libraries. No `./configure` step is needed. + +Dune will get confused if it finds leftovers of in-tree compilation, +so please be sure your tree is clean from objects files generated by +the make-based system. + +If you want to build the standard libraries and plugins you should +call `make -f Makefile.dune voboot`. It is usually enough to do that +once per-session. + +More helper targets are availabe in `Makefile.dune`, `make -f +Makefile.dune` will display help. + Dune ==== |