diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 49e71fe885bf0d51bcdd156ffa4774e04792357c..5a8f25c9a205badaa47f5d588f5752d1a3c1d6c7 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -99,8 +99,7 @@ check-opam-release: ################################################################################ ### PRE-RELEASE -make-manual: - <<: *when_release +.build-template: &make_manual stage: prepare-release variables: OUT: "manual" @@ -111,6 +110,14 @@ make-manual: script: - ./nix/ci.sh +release-manual: + <<: *when_release + <<: *make_manual + +force-manual: + <<: *manual_template + <<: *make_manual + check-versions: <<: *when_release stage: prepare-release