diff options
| author | Théo Zimmermann | 2019-03-13 10:38:03 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-03-13 10:38:03 +0100 |
| commit | 915192abdf1bdb3129fd28f05cee6340d5a8c464 (patch) | |
| tree | b526c4305b1ec13f8e69075a5ae46ba0293b2596 /dev/doc | |
| parent | e341c36cdc2aa2220152b2a3745bf3255316cdf3 (diff) | |
| parent | 430851db6db8ba30280f024ccbca5f6124287ab7 (diff) | |
Merge PR #9748: [dune] Add shim for coqtop.byte
Reviewed-by: Zimmi48
Reviewed-by: gares
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/build-system.dune.md | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index a31ab1c511..b1bfac8cc9 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -126,9 +126,9 @@ script again] This will be fixed in the future. ## Dropping from coqtop: -The following sequence is recommended: +After doing `make -f Makefile.dune voboot`, the following commands should work: ``` -dune exec coqtop.byte +dune exec dev/shim/coqbyte-prelude > Drop. # #directory "dev";; # #use "include_dune";; |