From c7d56372c7a2fff283fc4841f29cb0d5893aa431 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Sun, 22 Mar 2020 10:30:21 +0100
Subject: Fix deploy of refman following #11855.

---
 .gitlab-ci.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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
-- 
cgit v1.2.3


From 9252e89072239c8c1454e754f8498031dfacec54 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Sun, 22 Mar 2020 13:14:33 +0100
Subject: Fix world and watch targets of Makefile.dune now that doc has install
 rules.

---
 Makefile.dune | 6 ++++--
 1 file 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
-- 
cgit v1.2.3