From 2f2a3eb27c1d76b1943d2b08abb1fc3224109fb3 Mon Sep 17 00:00:00 2001
From: Andres Erbsen
Date: Tue, 26 Jun 2018 15:17:39 -0400
Subject: Add mit-plv/bedrock2-ci to CI

---
 dev/ci/ci-basic-overlay.sh | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'dev/ci/ci-basic-overlay.sh')

diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 2ebbf2cc4e..28321d13e2 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -147,6 +147,12 @@
 : "${bignums_CI_BRANCH:=master}"
 : "${bignums_CI_GITURL:=https://github.com/coq/bignums}"
 
+########################################################################
+# bedrock2
+########################################################################
+: "${bedrock2_CI_BRANCH:=master}"
+: "${bedrock2_CI_GITURL:=https://github.com/mit-plv/bedrock2}"
+
 ########################################################################
 # Equations
 ########################################################################
-- 
cgit v1.2.3