From f725580ecffa96cb0bfd526737586f7a36499286 Mon Sep 17 00:00:00 2001
From: Beta Ziliani
Date: Wed, 25 Apr 2018 14:17:51 -0300
Subject: updating CI for Mtac2

---
 dev/ci/ci-basic-overlay.sh |  6 +++---
 dev/ci/ci-metacoq.sh       | 19 -------------------
 dev/ci/ci-mtac2.sh         | 19 +++++++++++++++++++
 3 files changed, 22 insertions(+), 22 deletions(-)
 delete mode 100755 dev/ci/ci-metacoq.sh
 create mode 100755 dev/ci/ci-mtac2.sh

(limited to 'dev/ci')

diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 5566a51175..5cee72cc73 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -19,13 +19,13 @@
 : "${UniMath_CI_GITURL:=https://github.com/UniMath/UniMath.git}"
 
 ########################################################################
-# Unicoq + Metacoq
+# Unicoq + Mtac2
 ########################################################################
 : "${unicoq_CI_BRANCH:=master}"
 : "${unicoq_CI_GITURL:=https://github.com/unicoq/unicoq.git}"
 
-: "${metacoq_CI_BRANCH:=master}"
-: "${metacoq_CI_GITURL:=https://github.com/MetaCoq/MetaCoq.git}"
+: "${mtac2_CI_BRANCH:=master-sync}"
+: "${mtac2_CI_GITURL:=https://github.com/Mtac2/Mtac2.git}"
 
 ########################################################################
 # Mathclasses + Corn
diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-metacoq.sh
deleted file mode 100755
index a66dc1e762..0000000000
--- a/dev/ci/ci-metacoq.sh
+++ /dev/null
@@ -1,19 +0,0 @@
-#!/usr/bin/env bash
-
-ci_dir="$(dirname "$0")"
-. "${ci_dir}/ci-common.sh"
-
-unicoq_CI_DIR=${CI_BUILD_DIR}/unicoq
-metacoq_CI_DIR=${CI_BUILD_DIR}/MetaCoq
-
-# Setup UniCoq
-
-git_checkout "${unicoq_CI_BRANCH}" "${unicoq_CI_GITURL}" "${unicoq_CI_DIR}"
-
-( cd "${unicoq_CI_DIR}" && coq_makefile -f Make -o Makefile && make && make install )
-
-# Setup MetaCoq
-
-git_checkout "${metacoq_CI_BRANCH}" "${metacoq_CI_GITURL}" "${metacoq_CI_DIR}"
-
-( cd "${metacoq_CI_DIR}" && coq_makefile -f _CoqProject -o Makefile && make )
diff --git a/dev/ci/ci-mtac2.sh b/dev/ci/ci-mtac2.sh
new file mode 100755
index 0000000000..1372acb8e5
--- /dev/null
+++ b/dev/ci/ci-mtac2.sh
@@ -0,0 +1,19 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+unicoq_CI_DIR=${CI_BUILD_DIR}/unicoq
+mtac2_CI_DIR=${CI_BUILD_DIR}/Mtac2
+
+# Setup UniCoq
+
+git_checkout "${unicoq_CI_BRANCH}" "${unicoq_CI_GITURL}" "${unicoq_CI_DIR}"
+
+( cd "${unicoq_CI_DIR}" && coq_makefile -f Make -o Makefile && make && make install )
+
+# Setup MetaCoq
+
+git_checkout "${mtac2_CI_BRANCH}" "${mtac2_CI_GITURL}" "${mtac2_CI_DIR}"
+
+( cd "${mtac2_CI_DIR}" && coq_makefile -f _CoqProject -o Makefile && make )
-- 
cgit v1.2.3