From 94e783390ef9ad9d26a54add2287e0a3e58d1b70 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 24 May 2017 23:05:21 +0200
Subject: [location] [travis] Add overlays for located_switch

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

(limited to 'dev')

diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh
index 4ad5123170..28808a5814 100644
--- a/dev/ci/ci-user-overlay.sh
+++ b/dev/ci/ci-user-overlay.sh
@@ -26,9 +26,17 @@ echo $TRAVIS_BRANCH
 echo $TRAVIS_COMMIT
 
 if [ $TRAVIS_PULL_REQUEST == "402" ] || [ $TRAVIS_BRANCH == "located_switch" ]; then
+
     mathcomp_CI_BRANCH=located_switch
     mathcomp_CI_GITURL=https://github.com/ejgallego/math-comp.git
 
     fiat_parsers_CI_BRANCH=located_switch
     fiat_parsers_CI_GITURL=https://github.com/ejgallego/fiat.git
+
+    bedrock_src_CI_BRANCH=located_switch
+    bedrock_src_CI_GITURL=https://github.com/ejgallego/bedrock.git
+
+    bedrock_facade_CI_BRANCH=located_switch
+    bedrock_facade_CI_GITURL=https://github.com/ejgallego/bedrock.git
+
 fi
-- 
cgit v1.2.3