From d9d8977cf213f0d4b2e8d324c759c23df58ba457 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 21 Feb 2017 09:46:34 +0100
Subject: [travis] track an 8.7 specific branch of HoTT.

This is required since we merged PR#309: Ltac as a plugin.
---
 dev/ci/ci-hott.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh
index aaffc9d484..0c07564c02 100755
--- a/dev/ci/ci-hott.sh
+++ b/dev/ci/ci-hott.sh
@@ -3,6 +3,6 @@
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-git_checkout mz-8.6 https://github.com/ejgallego/HoTT.git HoTT
+git_checkout mz-8.7 https://github.com/ejgallego/HoTT.git HoTT
 
 ( cd HoTT && ./autogen.sh && ./configure && make -j ${NJOBS} )
-- 
cgit v1.2.3