diff options
| author | Michael Soegtrop | 2021-02-26 18:12:40 +0100 |
|---|---|---|
| committer | Michael Soegtrop | 2021-02-26 18:12:40 +0100 |
| commit | 6c14324577a434d36d8c81686c701a31936043a8 (patch) | |
| tree | 17e044456305aa1e402e8fb79146edd8a044d35e /.gitlab-ci.yml | |
| parent | 15074f171cdf250880bd0f7a2806356040c89f36 (diff) | |
CI Windows: adjust branch name to Coq Platform branch renaming
Diffstat (limited to '.gitlab-ci.yml')
| -rw-r--r-- | .gitlab-ci.yml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 6a8217674a..14bf263251 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -260,7 +260,7 @@ before_script: stage: stage-1 interruptible: true variables: - PLATFORM: "https://github.com/coq/platform/archive/master.zip" + PLATFORM: "https://github.com/coq/platform/archive/dev-ci.zip" artifacts: name: "$CI_JOB_NAME" paths: |