Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Remove use of "echo" and "cat" from flags/... generation
According to the dune metadata format [1], extra whitespace and newlines are not significant in a list, so remove the fragile use of "cat" from flags/ generation, replacing it with a single invocation of "sed". [1] https://dune.readthedocs.io/en/latest/project-layout-specification.html#metadata-format
- Loading branch information