aboutsummaryrefslogtreecommitdiff
path: root/dev/doc
diff options
context:
space:
mode:
Diffstat (limited to 'dev/doc')
-rw-r--r--dev/doc/build-system.dune.md7
1 files changed, 1 insertions, 6 deletions
diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md
index 0506216541..8b0bf216e3 100644
--- a/dev/doc/build-system.dune.md
+++ b/dev/doc/build-system.dune.md
@@ -18,10 +18,6 @@ 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 available in `Makefile.dune`, `make -f
Makefile.dune` will display some help.
@@ -55,7 +51,6 @@ Instead, you should use the provided "shims" for running `coqtop` and
`coqide` in a fast build. In order to use them, do:
```
-$ make -f Makefile.dune voboot # Only once per session
$ dune exec -- dev/shim/coqtop-prelude
```
@@ -153,7 +148,7 @@ depending on your OCaml version. This is due to several factors:
## Dropping from coqtop:
-After doing `make -f Makefile.dune voboot`, the following commands should work:
+The following commands should work:
```
dune exec -- dev/shim/coqbyte-prelude
> Drop.