diff options
| author | Enrico Tassi | 2020-12-04 15:05:40 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2020-12-04 15:05:40 +0100 |
| commit | 9fb840fa5f33f593bc204765a13c027155559c2e (patch) | |
| tree | 8d00d2284315308310043a7f9e4f3789a8c871a3 /dev/ci | |
| parent | 957fba5a176f74b397a3adf7c008e63145617b66 (diff) | |
[dune] [test-suite] pass BIN= as the regular makefile does
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions