Merged
Conversation
Closed
anmonteiro
approved these changes
Nov 26, 2022
Collaborator
anmonteiro
left a comment
There was a problem hiding this comment.
Thanks, this is a lot better than #6584.
- Added an optional suggestion
- TODOs to be fixed later?
src/dune_engine/source_tree.ml
Outdated
Comment on lines
+560
to
+562
| match file_exists with | ||
| | None -> None | ||
| | Some fname -> Some (Path.Source.relative path fname) |
Collaborator
There was a problem hiding this comment.
Suggested change
| match file_exists with | |
| | None -> None | |
| | Some fname -> Some (Path.Source.relative path fname) | |
| Option.map file_exists ~f:Path.Source.relative path |
Member
Author
|
The TODOs will indeed to be addressed later. |
The dune file path returned by Source_tree.Dune_file is always present. This is wrong because some dune files are generated using subdir. This commit tweaks the API to reflect this fact and updates the rest of the code to handle such virtual dune files. Signed-off-by: Rudi Grinberg <me@rgrinberg.com> ps-id: b2dfc4df-ea48-491c-987e-b9b3d193e597
986c099 to
e912144
Compare
moyodiallo
pushed a commit
to moyodiallo/dune
that referenced
this pull request
Dec 2, 2022
The dune file path returned by Source_tree.Dune_file is always present. This is wrong because some dune files are generated using subdir. This commit tweaks the API to reflect this fact and updates the rest of the code to handle such virtual dune files. Signed-off-by: Rudi Grinberg <me@rgrinberg.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The dune file path returned by Source_tree.Dune_file is always present.
This is wrong because some dune files are generated using subdir. This
commit tweaks the API to reflect this fact and updates the rest of the
code to handle such virtual dune files.
Signed-off-by: Rudi Grinberg me@rgrinberg.com
ps-id: b2dfc4df-ea48-491c-987e-b9b3d193e597