aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2020-04-30 14:10:16 +0200
committerPierre-Marie Pédrot2020-04-30 14:10:16 +0200
commitd436c45a19de2f91aad94f492b547225f8c5b305 (patch)
treeb666e829b6545ba38170dcf79276714dd89cbe32 /dev/ci
parent010ef152611977770fa137ed5980205d412febe5 (diff)
parent7a4e7dfbaa8dc3fa92931c4bfa39d268940e08f8 (diff)
Merge PR #12107: Remove mod_constraints field of module body
Reviewed-by: ppedrot
Diffstat (limited to 'dev/ci')
-rw-r--r--dev/ci/user-overlays/12107-SkySkimmer-no-mod-univs.sh6
1 files changed, 6 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/12107-SkySkimmer-no-mod-univs.sh b/dev/ci/user-overlays/12107-SkySkimmer-no-mod-univs.sh
new file mode 100644
index 0000000000..b5faabcfe1
--- /dev/null
+++ b/dev/ci/user-overlays/12107-SkySkimmer-no-mod-univs.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "12107" ] || [ "$CI_BRANCH" = "no-mod-univs" ]; then
+
+ elpi_CI_REF=no-mod-univs
+ elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi
+
+fi