diff options
| author | Théo Zimmermann | 2019-03-29 16:44:41 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-03-29 16:44:41 +0100 |
| commit | 6c6948ad61447d1a019d94b5ffed21e0e36e3d75 (patch) | |
| tree | 969484b3db9ecebebb2b6ac0c8fdc644b8d1e5f1 | |
| parent | 379781acc56c430485088e6d67785d420fa69691 (diff) | |
| parent | 5c7a943719429f18c567e2562f42ca90b999ff35 (diff) | |
Merge PR #9859: [dune] Don't regenerate ltac/dune after bootstrapping.
Reviewed-by: Zimmi48
| -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 |