diff options
| author | Gaëtan Gilbert | 2018-11-09 19:28:14 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-20 13:02:34 +0100 |
| commit | 7aeddf5cbf5755dab1cdcbab832c3d51a02c6c84 (patch) | |
| tree | 90492e47dca70b21c746938e353c95ec3c0e73af /dev/dune | |
| parent | d7172fbf2d7ae98ea0471a58c21f93671280d50e (diff) | |
dune: link kernel in checker instead of copying files
This allows to use the nice printers with constrextern etc, and since
we were copying everything we're not linking any more than previously.
Also the dune file is simpler without the copies.
Diffstat (limited to 'dev/dune')
0 files changed, 0 insertions, 0 deletions