diff options
| author | Emilio Jesus Gallego Arias | 2018-10-02 04:20:33 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-02 04:27:15 +0200 |
| commit | b46668fa43bb97f7d696978f687db3c97224ce4f (patch) | |
| tree | 1eca21761b0a3d7b5621b0c43ee890d4390ad0a3 /.github | |
| parent | ec751f0d48fa3d6268ed4210d74efac23bc87cbc (diff) | |
[dune] Install more files from `tools`.
These are needed for example for the test suite.
Diffstat (limited to '.github')
0 files changed, 0 insertions, 0 deletions