aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorEnrico Tassi2019-05-13 14:44:27 +0200
committerEnrico Tassi2019-05-13 14:44:27 +0200
commit34fbc9cc6b30fc8e7dc2bd37756d5ede29074de0 (patch)
treec59e91fc8ad41df8e5bd4280c44cc6da3cd20ffa /dev
parentcfecef471c706beb50d70b951b148c9629a4064a (diff)
parent4895bf8bb5d0acfaee499991973fc6537657427d (diff)
Merge PR #10076: [Canonical structures] Annotation to field declarations to prevent them from being “canonical”
Ack-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: gares Ack-by: maximedenes Ack-by: robbertkrebbers Ack-by: vbgl
Diffstat (limited to 'dev')
-rw-r--r--dev/ci/user-overlays/10076-vbgl-canonical-disable-hint.sh6
1 files changed, 6 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/10076-vbgl-canonical-disable-hint.sh b/dev/ci/user-overlays/10076-vbgl-canonical-disable-hint.sh
new file mode 100644
index 0000000000..2015935dd9
--- /dev/null
+++ b/dev/ci/user-overlays/10076-vbgl-canonical-disable-hint.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "10076" ] || [ "$CI_BRANCH" = "canonical-disable-hint" ]; then
+
+ elpi_CI_REF=canonical-disable-hint
+ elpi_CI_GITURL=https://github.com/vbgl/coq-elpi
+
+fi