diff options
| author | Enrico Tassi | 2020-12-08 11:41:32 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2021-01-05 10:38:52 +0100 |
| commit | 16cd0d5cfc0c4702b8220dad8e91f31a89d904ba (patch) | |
| tree | 0bab12b73d35f9ac938432b6d60042ef632d91f4 /.gitlab-ci.yml | |
| parent | fa7c0f9d55a5a33a0f76ddb0c5794a06117c6914 (diff) | |
[ci] windows job based on the platform
Diffstat (limited to '.gitlab-ci.yml')
| -rw-r--r-- | .gitlab-ci.yml | 28 |
1 files changed, 10 insertions, 18 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index bf3ac7a727..754c09776e 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -256,23 +256,18 @@ before_script: OPAM_SWITCH: "edge" OPAM_VARIANT: "+flambda" -.windows-template: +.platform-template: stage: stage-1 interruptible: true + variables: + PLATFORM: "https://github.com/coq/platform/archive/master.zip" artifacts: - name: "%CI_JOB_NAME%" + name: "$CI_JOB_NAME" paths: - artifacts when: always expire_in: 1 week - tags: - - windows-inria - before_script: [] - script: - - call dev/ci/gitlab.bat - only: - variables: - - $WINDOWS =~ /enabled/ + before_script: [] # We don't want to use the shared 'before_script' .deploy-template: stage: deploy @@ -349,16 +344,13 @@ build:quick: when: always windows64: - extends: .windows-template + extends: .platform-template variables: ARCH: "64" - -windows32: - extends: .windows-template - variables: - ARCH: "32" - except: - - /^pr-.*$/ + script: + - call dev/ci/platform-windows.bat + tags: + - windows-inria lint: stage: stage-1 |