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