diff options
| author | Emilio Jesus Gallego Arias | 2018-10-01 05:19:36 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-11 14:32:13 +0200 |
| commit | dc5dbc992727fb807fa56763f8f71d79f598fd6a (patch) | |
| tree | 494f0e418e6da50fc630d33700ac5376effc6680 /dune | |
| parent | aa5cdbd67b160417fe353a79393a89ed99481548 (diff) | |
[configure] Use absolute path for prefix.
Diffstat (limited to 'dune')
0 files changed, 0 insertions, 0 deletions