aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2018-12-16 13:54:40 +0100
committerPierre-Marie Pédrot2018-12-16 13:54:40 +0100
commit7e155688331c8f004f34950da67108d7284e4e56 (patch)
tree9182191cd348bc32eaa8cdd00b615a924ed17c6f /dev
parent2a7992f75c86a15512568ac61ca4c43e23242b28 (diff)
parenta2549c7f716e870ea19fdbfd7b5493117fe21e76 (diff)
Merge PR #9172: [proof] Rework proof interface.
Diffstat (limited to 'dev')
-rw-r--r--dev/ci/user-overlays/09172-ejgallego-proof_rework.sh9
1 files changed, 9 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/09172-ejgallego-proof_rework.sh b/dev/ci/user-overlays/09172-ejgallego-proof_rework.sh
new file mode 100644
index 0000000000..f532fdfc52
--- /dev/null
+++ b/dev/ci/user-overlays/09172-ejgallego-proof_rework.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "9172" ] || [ "$CI_BRANCH" = "proof_rework" ]; then
+
+ ltac2_CI_REF=proof_rework
+ ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
+
+ mtac2_CI_REF=proof_rework
+ mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2
+
+fi