diff options
| author | Emilio Jesus Gallego Arias | 2019-03-28 16:50:25 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-03-28 16:50:25 +0100 |
| commit | 5c7a943719429f18c567e2562f42ca90b999ff35 (patch) | |
| tree | 689d7f900adc6fbeb7dafb078b935955fa7603f5 /doc/plugin_tutorial/tuto3 | |
| parent | 688e20c432d2639050a62703e1c566ddfbe42b2a (diff) | |
[dune] Don't regenerate ltac/dune after bootstrapping.
Once we have the good `plugins/ltac/dune` in place for bootstrapping,
we should not regenerate it. Thanks to @maximedenes for the report.
This fixes `make states` always rebuilding ltac's dependencies.
Diffstat (limited to 'doc/plugin_tutorial/tuto3')
0 files changed, 0 insertions, 0 deletions