diff options
Diffstat (limited to 'Makefile.dune')
| -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 |