From c176063e57d1555fa7acd273dd151e35a01e58d1 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 7 Feb 2017 15:38:54 +0100
Subject: [travis] [External CI] iris-coq: fix dependencies

---
 dev/ci/ci-iris-coq.sh | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'dev')

diff --git a/dev/ci/ci-iris-coq.sh b/dev/ci/ci-iris-coq.sh
index c1306e070d..e97e2c19e3 100755
--- a/dev/ci/ci-iris-coq.sh
+++ b/dev/ci/ci-iris-coq.sh
@@ -24,6 +24,11 @@ git clone --depth 1 https://github.com/math-comp/math-comp.git
 # echo "Add ML Path \"`pwd`/math-comp/mathcomp/\"." > ${HOME}/.coqrc
 # echo "Add LoadPath \"`pwd`/math-comp/mathcomp/\" as mathcomp." >> ${HOME}/.coqrc
 
+# Setup stdpp
+git clone --depth 1 https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git
+
+( cd coq-stdpp && make -j ${NJOBS} && make install )
+
 # Setup Iris
 git clone --depth 1 https://gitlab.mpi-sws.org/FP/iris-coq.git
 
-- 
cgit v1.2.3