diff options
| author | Gaëtan Gilbert | 2019-10-04 13:33:33 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-10-04 14:07:15 +0200 |
| commit | 17a1bd7affa439a9a79ecdc34266dd235835192d (patch) | |
| tree | 7ff1f01119357c0017708b6c097adc5dec6db42e /dev/ci | |
| parent | d7f43705e347f728d99e45720d8f2e0a3f7cff34 (diff) | |
overlays for sprop default on
Diffstat (limited to 'dev/ci')
| -rw-r--r-- | dev/ci/user-overlays/10811-SkySkimmer-sprop-default-on.sh | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/10811-SkySkimmer-sprop-default-on.sh b/dev/ci/user-overlays/10811-SkySkimmer-sprop-default-on.sh new file mode 100644 index 0000000000..d7af6b7a36 --- /dev/null +++ b/dev/ci/user-overlays/10811-SkySkimmer-sprop-default-on.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "10811" ] || [ "$CI_BRANCH" = "sprop-default-on" ]; then + + elpi_CI_REF=sprop-default-on + elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi + + coq_dpdgraph_CI_REF=sprop-default-on + coq_dpdgraph_CI_GITURL=https://github.com/SkySkimmer/coq-dpdgraph + +fi |