diff options
| author | Théo Zimmermann | 2018-10-01 13:25:41 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-10-01 13:25:41 +0200 |
| commit | e315f7b3e3e31eda27ef9f752d58aa85707f77bd (patch) | |
| tree | 03427beaec973659ca82e35ded2903aeb423329c /dev/ci | |
| parent | 6a800b15ebd26131f59605e9c8cdcd5bfec15f0d (diff) | |
| parent | 2b2b10cd5bf017d9b69076ea98e4a1cb77fdbc00 (diff) | |
Merge PR #8606: [dune] [configure] Fix typo in default prefix setting.
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions