diff options
| author | Emilio Jesus Gallego Arias | 2018-12-06 05:21:18 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-12-10 16:00:41 +0100 |
| commit | 6aba0471154d68bbd40a512f741a10f32948d80f (patch) | |
| tree | 3f673b9ffb341759177ca0754ee568b550819b42 /dev/core.dbg | |
| parent | 10b07a187522b74bbcc9355d3ff9c4153f300706 (diff) | |
[dune] Teach coq_dune about `.glob` and `.aux` files.
This is a required step in order to be able to call `coqdoc` an
generate the documentation of the stdlib, and also useful for other
uses such as the asynchronous engine.
Diffstat (limited to 'dev/core.dbg')
0 files changed, 0 insertions, 0 deletions