Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
makefile: fix sed --promote-install-files dune arg retrieving
Get only the option itself in help, don't get appearing ones in text blocks
- Loading branch information