From 2470182ac4bded5c433c8f6bc77eb7b96576dc8d Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Tue, 13 Jun 2017 14:48:22 +0200
Subject: [travis] overlays for CompCert and VST (an extra Require Export
 FunInd)

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

(limited to 'dev/ci')

diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh
index 200d431bcb..62c245b4fe 100644
--- a/dev/ci/ci-user-overlay.sh
+++ b/dev/ci/ci-user-overlay.sh
@@ -47,3 +47,10 @@ if [ $TRAVIS_PULL_REQUEST == "498" ] || [ $TRAVIS_BRANCH == "outsource-bignums"
     Corn_CI_BRANCH=external-bignums
     Corn_CI_GITURL=https://github.com/letouzey/corn.git
 fi
+
+if [ $TRAVIS_PULL_REQUEST == "220" ] || [ $TRAVIS_BRANCH == "less_init_plugins" ]; then
+    CompCert_CI_BRANCH=less_init_plugins
+    CompCert_CI_GITURL=https://github.com/letouzey/CompCert.git
+    VST_CI_BRANCH=less_init_plugins
+    VST_CI_GITURL=https://github.com/letouzey/VST.git
+fi
-- 
cgit v1.2.3