aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2018-11-21 13:03:27 +0100
committerPierre-Marie Pédrot2018-11-21 13:03:27 +0100
commit4d0fea2ededb11d79f4f1abcc1595f9cec20d6dd (patch)
treebbd47886f4649999ecad9f21ffb6ff55869f0132 /dev/ci
parent968be14b3788e112425eedf696f2e5e35d35ba17 (diff)
parent417641e48129c9ba8656c622c9b64cd32641e7de (diff)
Merge PR #8998: [legacy proof engine] Remove some cruft.
Diffstat (limited to 'dev/ci')
-rw-r--r--dev/ci/user-overlays/08998-ejgallego-legacy_proof_eng_clean.sh6
1 files changed, 6 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/08998-ejgallego-legacy_proof_eng_clean.sh b/dev/ci/user-overlays/08998-ejgallego-legacy_proof_eng_clean.sh
new file mode 100644
index 0000000000..c8bea0c868
--- /dev/null
+++ b/dev/ci/user-overlays/08998-ejgallego-legacy_proof_eng_clean.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "8998" ] || [ "$CI_BRANCH" = "legacy_proof_eng_clean" ]; then
+
+ equations_CI_REF=legacy_proof_eng_clean
+ equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+fi