FIX: Pipeline: Remove `/public/` if it exists.

36abb5e5 · Daniel · b25c6a67 · 36abb5e5
Unverified Commit 36abb5e5 authored 4 years ago by Daniel
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -109,7 +109,7 @@ pages:
  script:
    - echo "Deploying"
    - make doc
-    - cp -r build/doc/html public
+    - {rm public || true}; cp -r build/doc/html public
  artifacts:
    paths:
      - public