diff options
| author | Pierre Roux | 2019-11-10 16:12:04 +0100 |
|---|---|---|
| committer | Pierre Roux | 2019-11-11 17:43:23 +0100 |
| commit | 09b39c339dd3fe21a0808097b5f7d1ab8cb47031 (patch) | |
| tree | 40eb1aa01c8ffbc4531c5a4227c07d50b8051bdb /dev | |
| parent | 69b91851ed5d18f1ca34ef2597f0cf342c10a124 (diff) | |
Have only one dune rule calling configure
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions