From 928bced545407a2043fe2acaa5b31b1aa07988d5 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 7 May 2019 14:43:55 +0200
Subject: Remove ppedrot/ltac2 from CI after integration in main repo

---
 dev/ci/ci-basic-overlay.sh | 7 -------
 dev/ci/ci-ltac2.sh         | 8 --------
 2 files changed, 15 deletions(-)
 delete mode 100755 dev/ci/ci-ltac2.sh

(limited to 'dev')

diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 4f5988c59c..f97e781832 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -80,13 +80,6 @@
 : "${coqhammer_CI_GITURL:=https://github.com/lukaszcz/coqhammer}"
 : "${coqhammer_CI_ARCHIVEURL:=${coqhammer_CI_GITURL}/archive}"
 
-########################################################################
-# Ltac2
-########################################################################
-: "${ltac2_CI_REF:=master}"
-: "${ltac2_CI_GITURL:=https://github.com/ppedrot/ltac2}"
-: "${ltac2_CI_ARCHIVEURL:=${ltac2_CI_GITURL}/archive}"
-
 ########################################################################
 # GeoCoq
 ########################################################################
diff --git a/dev/ci/ci-ltac2.sh b/dev/ci/ci-ltac2.sh
deleted file mode 100755
index 4df22bf249..0000000000
--- a/dev/ci/ci-ltac2.sh
+++ /dev/null
@@ -1,8 +0,0 @@
-#!/usr/bin/env bash
-
-ci_dir="$(dirname "$0")"
-. "${ci_dir}/ci-common.sh"
-
-git_download ltac2
-
-( cd "${CI_BUILD_DIR}/ltac2" && make && make tests && make install )
-- 
cgit v1.2.3