From 3039bb02e0029b771cc904a5806b5cb8f99d6c49 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 20 Jul 2020 11:04:21 +0200
Subject: CI: deploy make-built stdlib doc

Workaround #12699
Alternative to #12700
---
 .gitlab-ci.yml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 3b95800f0d..ec8fe23171 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -481,6 +481,8 @@ doc:refman-pdf:dune:
       - _build/log
       - _build/default/doc/refman-pdf
 
+# currently bugged: dune cleans up the glob files so no links
+# see #12699
 doc:stdlib:dune:
   extends: .dune-ci-template
   variables:
@@ -501,11 +503,11 @@ doc:refman:deploy:
   dependencies:
     - doc:ml-api:odoc
     - doc:refman:dune
-    - doc:stdlib:dune
+    - build:base
   needs:
     - doc:ml-api:odoc
     - doc:refman:dune
-    - doc:stdlib:dune
+    - build:base
   script:
     - echo "$DOCUMENTATION_DEPLOY_KEY" | tr -d '\r' | ssh-add - > /dev/null
     - git clone git@github.com:coq/doc.git _deploy
@@ -515,7 +517,7 @@ doc:refman:deploy:
     - mkdir -p _deploy/$CI_COMMIT_REF_NAME
     - cp -rv _build/default/_doc/_html _deploy/$CI_COMMIT_REF_NAME/api
     - 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
+    - cp -rv _install_ci/share/doc/coq/html/stdlib _deploy/$CI_COMMIT_REF_NAME/stdlib
     - cd _deploy/$CI_COMMIT_REF_NAME/
     - git add api refman stdlib
     - git commit -m "Documentation of branch “$CI_COMMIT_REF_NAME” at $CI_COMMIT_SHORT_SHA"
-- 
cgit v1.2.3