diff options
| author | Emilio Jesus Gallego Arias | 2018-11-09 18:29:08 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-09 18:29:08 +0100 |
| commit | 09db499e23b0e47254c285f3ab51986e87e78641 (patch) | |
| tree | 2076e31228f8e05d2194cb12fb899f0c028abfe7 /dev/tools/pre-commit | |
| parent | 1761f8ed41f3891f8b6edc0dd256cd18e47a74fb (diff) | |
[dune] Build `cmxs` files instead of `cmxa` in "quick" target.
This fixes #8954
Diffstat (limited to 'dev/tools/pre-commit')
0 files changed, 0 insertions, 0 deletions