aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2018-11-16 20:16:41 +0100
committerEmilio Jesus Gallego Arias2018-11-21 01:26:45 +0100
commit417641e48129c9ba8656c622c9b64cd32641e7de (patch)
treebbd47886f4649999ecad9f21ffb6ff55869f0132 /dev/ci
parent968be14b3788e112425eedf696f2e5e35d35ba17 (diff)
[legacy proof engine] Remove some cruft.
We remove the `Proof_types` file which was a trivial stub, we also cleanup a few layers of aliases. This is not a lot but every little step helps.
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