diff options
Diffstat (limited to 'dune-project')
| -rw-r--r-- | dune-project | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/dune-project b/dune-project index b7399d2..cc3ce88 100644 --- a/dune-project +++ b/dune-project | |||
| @@ -4,6 +4,10 @@ | |||
| 4 | 4 | ||
| 5 | (generate_opam_files true) | 5 | (generate_opam_files true) |
| 6 | 6 | ||
| 7 | ; Needed to generate correct debug information. | ||
| 8 | ; See https://dune.readthedocs.io/en/stable/dune-files.html#stanza-map_workspace_root | ||
| 9 | (map_workspace_root false) | ||
| 10 | |||
| 7 | (source | 11 | (source |
| 8 | (github username/reponame)) | 12 | (github username/reponame)) |
| 9 | 13 | ||