diff options
| author | Gaëtan Gilbert | 2020-03-25 13:20:55 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-03-25 13:20:55 +0100 |
| commit | f8de4874c44a24fa107ec6089ae4914821e359a8 (patch) | |
| tree | 0ceebdedb6981db308825737b6246223e3d0e845 /Makefile.dune | |
| parent | bc70bb31c579b9482d0189f20806632c62b26a61 (diff) | |
| parent | 9252e89072239c8c1454e754f8498031dfacec54 (diff) | |
Merge PR #11875: Fix deploy of refman following #11855.
Reviewed-by: SkySkimmer
Ack-by: ejgallego
Diffstat (limited to 'Makefile.dune')
| -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 |