Summary: Move definitions of profiles from `dune-workspace` to `dune` since it seems to be ok to use profiles in `dune-workspace` that are only defined in `dune`. Since the `dune` but not `dune-workspace` file is used when building as a vendored dependency, this seems to be preferable. Also, change the `opt` profile into a wildcard, which seems to be preferable from the vendored-building perspective. Also, set library public names such that including `sledge` in the `libraries` phrase of `dune` files works. Reviewed By: ngorogiannis Differential Revision: D20376179 fbshipit-source-id: f2b634716master
parent
8337097cf0
commit
134f9f930e
Loading…
Reference in new issue