aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2019-08-21 15:14:02 +0200
committerEmilio Jesus Gallego Arias2019-08-21 15:14:02 +0200
commit6bb04f3240e14cc0bbb117879afd0305db31b64c (patch)
tree6192b2186862c228ebf900e3cf6e4fe29c28eb30
parentc4793e587a11c5509e5bfa55d6f87f2d19afa9f9 (diff)
parent60f0b23aaf176fcc319455677c6c678b980ee3de (diff)
Merge PR #10678: [ci] Remove dead code.
Reviewed-by: ejgallego
-rw-r--r--Makefile.ci2
-rwxr-xr-xdev/ci/ci-cpdt.sh9
-rwxr-xr-xdev/ci/ci-tlc.sh9
3 files changed, 0 insertions, 20 deletions
diff --git a/Makefile.ci b/Makefile.ci
index 677fd734bf..de03ee8e84 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -18,7 +18,6 @@ CI_TARGETS= \
ci-coq_dpdgraph \
ci-coquelicot \
ci-corn \
- ci-cpdt \
ci-cross-crypto \
ci-elpi \
ci-ext-lib \
@@ -41,7 +40,6 @@ CI_TARGETS= \
ci-sf \
ci-simple-io \
ci-stdlib2 \
- ci-tlc \
ci-unimath \
ci-verdi-raft \
ci-vst
diff --git a/dev/ci/ci-cpdt.sh b/dev/ci/ci-cpdt.sh
deleted file mode 100755
index ca759c7b39..0000000000
--- a/dev/ci/ci-cpdt.sh
+++ /dev/null
@@ -1,9 +0,0 @@
-#!/usr/bin/env bash
-
-ci_dir="$(dirname "$0")"
-. "${ci_dir}/ci-common.sh"
-
-wget http://adam.chlipala.net/cpdt/cpdt.tgz
-tar xvfz cpdt.tgz
-
-( cd cpdt && make clean && make )
diff --git a/dev/ci/ci-tlc.sh b/dev/ci/ci-tlc.sh
deleted file mode 100755
index a2f0bea555..0000000000
--- a/dev/ci/ci-tlc.sh
+++ /dev/null
@@ -1,9 +0,0 @@
-#!/usr/bin/env bash
-
-ci_dir="$(dirname "$0")"
-. "${ci_dir}/ci-common.sh"
-
-FORCE_GIT=1
-git_download tlc
-
-( cd "${CI_BUILD_DIR}/tlc" && make )