Merge PR coq#20057: Deploy Corelib doc

Reviewed-by: Zimmi48 Co-authored-by: Zimmi48 <[email protected]>
SkySkimmer · Jan 15, 2025 · f3c7766 · f3c7766
2 parents 8a75617 + 4225caa
commit f3c7766
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
@@ -486,11 +486,11 @@ 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/corelib/html _deploy/$CI_COMMIT_REF_NAME/init
+    - cp -rv _build/default/doc/corelib/html _deploy/$CI_COMMIT_REF_NAME/corelib
     - cp -rv _build_ci/stdlib/_build/default/doc/refman-html _deploy/$CI_COMMIT_REF_NAME/refman-stdlib
     - cp -rv _build_ci/stdlib/_build/default/doc/stdlib/html _deploy/$CI_COMMIT_REF_NAME/stdlib
     - cd _deploy/$CI_COMMIT_REF_NAME/
-    - git add api refman stdlib
+    - git add api refman corelib refman-stdlib stdlib
     - git commit -m "Documentation of branch “$CI_COMMIT_REF_NAME” at $CI_COMMIT_SHORT_SHA"
     - git push # TODO: rebase and retry on failure