aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
diff options
context:
space:
mode:
Diffstat (limited to 'dev/ci')
-rw-r--r--dev/ci/ci-basic-overlay.sh16
-rwxr-xr-xdev/ci/ci-bedrock-facade.sh10
-rwxr-xr-xdev/ci/ci-bedrock-src.sh10
3 files changed, 2 insertions, 34 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 7f66dfb3b0..99ec43e412 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -13,8 +13,8 @@
########################################################################
# UniMath
########################################################################
-: ${UniMath_CI_BRANCH:=coq_makefile2-fix}
-: ${UniMath_CI_GITURL:=https://github.com/maximedenes/UniMath.git}
+: ${UniMath_CI_BRANCH:=master}
+: ${UniMath_CI_GITURL:=https://github.com/UniMath/UniMath.git}
########################################################################
# Unicoq + Metacoq
@@ -95,18 +95,6 @@
: ${fiat_crypto_CI_GITURL:=https://github.com/letouzey/fiat-crypto.git}
########################################################################
-# bedrock_src
-########################################################################
-: ${bedrock_src_CI_BRANCH:=master}
-: ${bedrock_src_CI_GITURL:=https://github.com/mit-plv/bedrock.git}
-
-########################################################################
-# bedrock_facade
-########################################################################
-: ${bedrock_facade_CI_BRANCH:=master}
-: ${bedrock_facade_CI_GITURL:=https://github.com/mit-plv/bedrock.git}
-
-########################################################################
# formal-topology
########################################################################
: ${formal_topology_CI_BRANCH:=ci}
diff --git a/dev/ci/ci-bedrock-facade.sh b/dev/ci/ci-bedrock-facade.sh
deleted file mode 100755
index 95cfa3073f..0000000000
--- a/dev/ci/ci-bedrock-facade.sh
+++ /dev/null
@@ -1,10 +0,0 @@
-#!/usr/bin/env bash
-
-ci_dir="$(dirname "$0")"
-source ${ci_dir}/ci-common.sh
-
-bedrock_facade_CI_DIR=${CI_BUILD_DIR}/bedrock-facade
-
-git_checkout ${bedrock_facade_CI_BRANCH} ${bedrock_facade_CI_GITURL} ${bedrock_facade_CI_DIR}
-
-( cd ${bedrock_facade_CI_DIR} && make -j ${NJOBS} facade )
diff --git a/dev/ci/ci-bedrock-src.sh b/dev/ci/ci-bedrock-src.sh
deleted file mode 100755
index 532611d4b3..0000000000
--- a/dev/ci/ci-bedrock-src.sh
+++ /dev/null
@@ -1,10 +0,0 @@
-#!/usr/bin/env bash
-
-ci_dir="$(dirname "$0")"
-source ${ci_dir}/ci-common.sh
-
-bedrock_src_CI_DIR=${CI_BUILD_DIR}/bedrock-src
-
-git_checkout ${bedrock_src_CI_BRANCH} ${bedrock_src_CI_GITURL} ${bedrock_src_CI_DIR}
-
-( cd ${bedrock_src_CI_DIR} && make -j ${NJOBS} src )