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 7113feb commit 56867a3
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 @@ -442,7 +442,7 @@ false)``
map_workspace_root
-------------------

It is desirable that the output of tools not contain references to the
The desirable output of tools will not contain references to the
file system location from which they were built. Starting from Dune 3.6,
Dune has mapped references to the workspace directory to "/workspace_root".

Expand Down

0 comments on commit 56867a3

Please sign in to comment.