diff options
| author | Théo Zimmermann | 2020-03-22 13:14:33 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-03-24 11:22:45 +0100 |
| commit | 9252e89072239c8c1454e754f8498031dfacec54 (patch) | |
| tree | 62eba55646f12a2e21312787adcf6bb93270afdd | |
| parent | c7d56372c7a2fff283fc4841f29cb0d5893aa431 (diff) | |
Fix world and watch targets of Makefile.dune now that doc has install rules.
| -rw-r--r-- | Makefile.dune | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/Makefile.dune b/Makefile.dune index 0520d43da9..b77e78db69 100644 --- a/Makefile.dune +++ b/Makefile.dune @@ -54,8 +54,10 @@ voboot: plugins/ltac/dune states: voboot dune build --display=short $(DUNEOPT) dev/shim/coqtop-prelude +NONDOC_INSTALL_TARGETS:=coq.install coqide-server.install coqide.install + world: voboot - dune build $(DUNEOPT) @install + dune build $(DUNEOPT) $(NONDOC_INSTALL_TARGETS) coq: voboot dune build $(DUNEOPT) coq.install @@ -67,7 +69,7 @@ coqide-server: voboot dune build $(DUNEOPT) coqide-server.install watch: voboot - dune build $(DUNEOPT) @install -w + dune build $(DUNEOPT) $(NONDOC_INSTALL_TARGETS) -w check: voboot dune build $(DUNEOPT) @check |