From fad095ccc656c5fccc5e50b36067deabde233bb3 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 12 Feb 2019 04:32:47 +0100
Subject: [dev] Add include versions for Dune builds.

Fixes #9537

This way, users can do:
```
dune exec coqtop.byte
> Drop.
 # #directory "dev";;
 # #use "include_dune";;
```
---
 dev/doc/build-system.dune.md | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'dev/doc')

diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md
index 01c32041d2..da91c85856 100644
--- a/dev/doc/build-system.dune.md
+++ b/dev/doc/build-system.dune.md
@@ -106,6 +106,16 @@ refined, so you need to build enough of Coq once to use this target
 [it will then correctly compute the deps and rebuild if you call the
 script again] This will be fixed in the future.
 
+## Dropping from coqtop:
+
+The following sequence is recommended:
+```
+dune exec coqtop.byte
+> Drop.
+# #directory "dev";;
+# #use "include_dune";;
+```
+
 ## Compositionality, developer and release modes.
 
 By default [in "developer mode"], Dune will compose all the packages
-- 
cgit v1.2.3