aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorcoqbot-app[bot]2021-02-26 18:08:08 +0000
committerGitHub2021-02-26 18:08:08 +0000
commit1e54fe53ac47f08d7b8f13df16487b5a2639404f (patch)
treef40dad08210864a76183cadb4b28bde960f37c94
parent4d93cebf19b2ac0ce162dad8c4c73d84ee7f4832 (diff)
parent6c14324577a434d36d8c81686c701a31936043a8 (diff)
Merge PR #13884: CI Windows: adjust branch name to Coq Platform branch renaming
Reviewed-by: gares
-rw-r--r--.gitlab-ci.yml2
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: