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 | |
| 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.
| -rw-r--r-- | Makefile.dune | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/Makefile.dune b/Makefile.dune index 4609c563d9..ebf74978a9 100644 --- a/Makefile.dune +++ b/Makefile.dune @@ -42,8 +42,10 @@ help: @echo " - help: show this message" # We need to bootstrap with a dummy coq.plugins.ltac so install targets do work. -voboot: +plugins/ltac/dune: @echo "(library (name ltac_plugin) (public_name coq.plugins.ltac) (modules_without_implementation extraargs extratactics))" > plugins/ltac/dune + +voboot: plugins/ltac/dune dune build $(DUNEOPT) @vodeps dune exec ./tools/coq_dune.exe $(BUILD_CONTEXT)/.vfiles.d |