diff options
Diffstat (limited to 'dev')
| -rwxr-xr-x | dev/ci/ci-cpdt.sh | 9 | ||||
| -rwxr-xr-x | dev/ci/ci-tlc.sh | 9 |
2 files changed, 0 insertions, 18 deletions
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 ) |