diff options
| author | Emilio Jesus Gallego Arias | 2018-09-27 16:02:31 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-09-27 16:51:58 +0200 |
| commit | 1a331405aa87c81eb51929557a7f3f10f8eabccf (patch) | |
| tree | 723a85723f3886af965ec9d4ff7a52dfd2b3ee51 /dev/header.c | |
| parent | 686503bfe85436e5af927a02f7e1fb0bf2f975c9 (diff) | |
[ci] Allow `make ci-$contrib` when we have a build under Dune.
This should allow people to test CI contribs under Dune. It should be
good for now but it is still a work in progress.
Diffstat (limited to 'dev/header.c')
0 files changed, 0 insertions, 0 deletions