Skip to content

Commit

Permalink
Update doc/dune-files.rst
Browse files Browse the repository at this point in the history
Co-authored-by: Christine Rose <[email protected]>
Signed-off-by: Richard L Ford <[email protected]>
  • Loading branch information
richardlford and christinerose authored Feb 6, 2023
1 parent 56867a3 commit 805e862
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion doc/dune-files.rst
Original file line number Diff line number Diff line change
Expand Up @@ -457,7 +457,7 @@ Starting with Dune 3.0, Dune does this mapping by default. However,
starting with Dune 3.7, this can be turned off using
``(map_workspace_root false)``
Note that when this mapping is enabled, the debug information produced
by the byte-code compiler is incorrect, as the location information
by the bytecode compiler is incorrect, as the location information
is lost.

.. _dune-files:
Expand Down

0 comments on commit 805e862

Please sign in to comment.