ci: drop `doc`; we have `pages` instead now

The `pages` job works.  We might consolidate this later,
also e.g. drop the doc dependencies from the default image
if we won't really use that image for docs anymore.

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 8015610b59e1f8da4fa3f1ef9a3203d30348b63c..99f22ddacd86eda43bc3dffaad4d184a785f8cca 100644 (file)
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -209,16 +209,6 @@ trivial_checks: # aggregated to save some processing
     - ci/no_assert_check.sh
     - ci/deckard_commit_check.sh
 
-doc:
-  <<: *sanity
-  script:
-    - meson build_doc -Ddoc=enabled
-    - ninja -C build_doc doc-strict
-  artifacts:
-    expire_in: 6 hour
-    paths:
-      - doc/html
-
 lint:other:
   <<: *sanity
   script: