aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorThéo Zimmermann2018-09-07 11:35:54 +0200
committerThéo Zimmermann2018-09-07 11:35:54 +0200
commit07c3905c30590c93f1b173833087bbd1df364227 (patch)
tree793df989971b55b25288cfc42b633ac4094f7c2f /dev
parent94c0c0403f8d0f705c49ed227affb0ba5fa544d7 (diff)
parentc8cc7a6901edf80638e7fcb4a9d22173e9523c96 (diff)
Merge PR #8426: [dune] [doc] Document `dune utop $lib`
Diffstat (limited to 'dev')
-rw-r--r--dev/doc/build-system.dune.md11
1 files changed, 11 insertions, 0 deletions
diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md
index 0b3e414513..85aaf317ef 100644
--- a/dev/doc/build-system.dune.md
+++ b/dev/doc/build-system.dune.md
@@ -39,6 +39,17 @@ In order to build a single package, you can do `dune build
$PACKAGE.install`. Dune also provides targets for documentation and
testing, see below.
+## Developer shell
+
+You can create a developer shell with `dune utop $library`, where
+`$library` can be any directory in the current workspace. For example,
+`dune utop engine` or `dune utop plugins/ltac` will launch `utop` with
+the right libraries already loaded.
+
+Note that you must invoke the `#rectypes;;` toplevel flag in order to
+use Coq libraries. The provided `.ocamlinit` file does this
+automatically.
+
## Compositionality, developer and release modes.
By default [in "developer mode"], Dune will compose all the packages