diff options
| author | Théo Zimmermann | 2018-09-21 16:22:32 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-09-21 16:22:32 +0200 |
| commit | 508265318ad39d2962587af4e10f79f4cf4cf4c6 (patch) | |
| tree | d4a32174d207668881e3de350863764760541f5f /plugins | |
| parent | 80b0619e81bec85e8f37b4ee9f8e4d5faa3eae13 (diff) | |
| parent | 81e4c7152da598c1750e7881b197a6fcf54e818d (diff) | |
Merge PR #8443: [opam] [dune] Fix typo + set prefix for configure.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions