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 | |
| parent | bc70bb31c579b9482d0189f20806632c62b26a61 (diff) | |
| parent | 9252e89072239c8c1454e754f8498031dfacec54 (diff) | |
Merge PR #11875: Fix deploy of refman following #11855.
Reviewed-by: SkySkimmer
Ack-by: ejgallego
| -rw-r--r-- | .gitlab-ci.yml | 2 | ||||
| -rw-r--r-- | Makefile.dune | 6 |
2 files changed, 5 insertions, 3 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index cf1dc47fab..ebeee0d4e4 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -470,7 +470,7 @@ doc:refman:deploy: - rm -rf _deploy/$CI_COMMIT_REF_NAME/stdlib - mkdir -p _deploy/$CI_COMMIT_REF_NAME - cp -rv _build/default/_doc/_html _deploy/$CI_COMMIT_REF_NAME/api - - cp -rv _build/default/doc/sphinx_build/html _deploy/$CI_COMMIT_REF_NAME/refman + - cp -rv _build/default/doc/refman-html _deploy/$CI_COMMIT_REF_NAME/refman - cp -rv _build/default/doc/stdlib/html _deploy/$CI_COMMIT_REF_NAME/stdlib - cd _deploy/$CI_COMMIT_REF_NAME/ - git add api refman stdlib 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 |