From 60f0b23aaf176fcc319455677c6c678b980ee3de Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 20 Aug 2019 13:38:59 +0200
Subject: [ci] Remove dead code.

TLC and CPDT are not actually tested. No point in keeping them as if they were.
---
 dev/ci/ci-cpdt.sh | 9 ---------
 dev/ci/ci-tlc.sh  | 9 ---------
 2 files changed, 18 deletions(-)
 delete mode 100755 dev/ci/ci-cpdt.sh
 delete mode 100755 dev/ci/ci-tlc.sh

(limited to 'dev')

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 )
-- 
cgit v1.2.3