aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
diff options
context:
space:
mode:
authorHugo Herbelin2020-02-11 16:06:45 +0100
committerHugo Herbelin2020-02-11 16:06:45 +0100
commit6975536db325a0f4dcbcb609dd8959d45fc19830 (patch)
tree895e71bd5d99d838c34eac7696ac3e539b7ca3bf /dev/ci
parent4c6c173447d5b7d04aa0fd4f51d27a078c675708 (diff)
parent2c9d58c4680dd3c60dacf387a7ea457584bec42f (diff)
Merge PR #11235: Add syntax for non maximal implicit arguments
Reviewed-by: herbelin Reviewed-by: jfehrle Ack-by: maximedenes
Diffstat (limited to 'dev/ci')
-rw-r--r--dev/ci/user-overlays/11235-non-maximal-implicit.sh9
1 files changed, 9 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/11235-non-maximal-implicit.sh b/dev/ci/user-overlays/11235-non-maximal-implicit.sh
new file mode 100644
index 0000000000..fd63980036
--- /dev/null
+++ b/dev/ci/user-overlays/11235-non-maximal-implicit.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "11235" ] || [ "$CI_BRANCH" = "non-maximal-implicit" ]; then
+
+ quickchick_CI_REF=non_maximal_implicit
+ quickchick_CI_GITURL=https://github.com/SimonBoulier/QuickChick
+
+ elpi_CI_REF=non_maximal_implicit
+ elpi_CI_GITURL=https://github.com/SimonBoulier/coq-elpi
+
+fi