diff options
| author | Emilio Jesus Gallego Arias | 2020-05-07 12:35:00 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-05-07 12:35:00 +0200 |
| commit | 18a78b53f6998d3af8f8bb1b7a6b5054af232d4e (patch) | |
| tree | 9de758c3074efee99d840ccfc7527e2b0d9cbe8e /dev/ci/user-overlays | |
| parent | 325a644b3f5a5f8c1a86191004576e7c763ae9f3 (diff) | |
| parent | bd69c92a0224918b1d4116a73841a67e72bccd8a (diff) | |
Merge PR #12267: [ci] bump elpi to 1.11
Diffstat (limited to 'dev/ci/user-overlays')
| -rw-r--r-- | dev/ci/user-overlays/12267-gares-elpi-1.11.sh | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/12267-gares-elpi-1.11.sh b/dev/ci/user-overlays/12267-gares-elpi-1.11.sh new file mode 100644 index 0000000000..ceb7afe3d1 --- /dev/null +++ b/dev/ci/user-overlays/12267-gares-elpi-1.11.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "12267" ] || [ "$CI_BRANCH" = "elpi-1.11" ]; then + + elpi_CI_REF="coq-master+elpi-1.11" + elpi_hb_CI_REF="coq-master+elpi.11" + +fi |