From bb6dbba6a76f83c7cbac7a1f8d6eaa14da2d3d40 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey <pierre.letouzey@inria.fr>
Date: Tue, 13 Jun 2017 15:47:56 +0200
Subject: [travis] overlay for fiat-crypto (a Require Import FunInd)

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

(limited to 'dev')

diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh
index 62c245b4f..2ecd40416 100644
--- a/dev/ci/ci-user-overlay.sh
+++ b/dev/ci/ci-user-overlay.sh
@@ -53,4 +53,6 @@ if [ $TRAVIS_PULL_REQUEST == "220" ] || [ $TRAVIS_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
+    fiat_crypto_CI_BRANCH=less_init_plugins
+    fiat_crypto_CI_GITURL=https://github.com/letouzey/fiat-crypto.git
 fi
-- 
cgit v1.2.3