diff options
| author | Emilio Jesus Gallego Arias | 2019-08-21 15:14:02 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-08-21 15:14:02 +0200 |
| commit | 6bb04f3240e14cc0bbb117879afd0305db31b64c (patch) | |
| tree | 6192b2186862c228ebf900e3cf6e4fe29c28eb30 | |
| parent | c4793e587a11c5509e5bfa55d6f87f2d19afa9f9 (diff) | |
| parent | 60f0b23aaf176fcc319455677c6c678b980ee3de (diff) | |
Merge PR #10678: [ci] Remove dead code.
Reviewed-by: ejgallego
| -rw-r--r-- | Makefile.ci | 2 | ||||
| -rwxr-xr-x | dev/ci/ci-cpdt.sh | 9 | ||||
| -rwxr-xr-x | dev/ci/ci-tlc.sh | 9 |
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 ) |
