Skip to content

Commit

Permalink
ci-refman does not actually depend on platform_full
Browse files Browse the repository at this point in the history
  • Loading branch information
SkySkimmer committed Dec 14, 2024
1 parent 4f65f0a commit 2506691
Show file tree
Hide file tree
Showing 2 changed files with 1 addition and 29 deletions.
28 changes: 0 additions & 28 deletions .gitlab-ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -1238,34 +1238,6 @@ doc:ci-refman:
needs:
- build:edge+flambda
- library:ci-stdlib+flambda
- plugin:ci-itauto
- plugin:ci-aac_tactics
- plugin:ci-bignums
- plugin:ci-coq_dpdgraph
- library:ci-coquelicot
- library:ci-corn
- library:ci-coqprime
- plugin:ci-elpi_hb
- library:ci-ext_lib
- plugin:ci-equations
- library:ci-flocq
- plugin:ci-coqhammer
- library:ci-hott
- library:ci-iris
- library:ci-math_classes
- library:ci-mathcomp
- library:ci-mathcomp_word
- library:ci-mczify
- library:ci-finmap
- library:ci-bigenough
- library:ci-analysis
- library:ci-menhir
- plugin:ci-mtac2
- plugin:ci-paramcoq
- plugin:ci-quickchick
- plugin:ci-reduction_effects
- plugin:ci-relation_algebra
- library:ci-simple_io
stage: build-3+
artifacts:
paths:
Expand Down
2 changes: 1 addition & 1 deletion Makefile.ci
Original file line number Diff line number Diff line change
Expand Up @@ -249,7 +249,7 @@ ci-verdi_raft: ci-stdlib

ci-waterproof: ci-stdlib

ci-refman: ci-platform_full
ci-refman: ci-stdlib

# Virtual targets used by the CI to group compilation of rules in a single job

Expand Down

0 comments on commit 2506691

Please sign in to comment.