From 56dc3e331c6b4b2bfa5ac072db57db8250884ce3 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
Date: Tue, 7 Mar 2017 12:33:37 +0100
Subject: Improve build of travis target on local machine.

- Move the git clones to a specific subfolder to avoid pollution.
- Do not fail when git clone already exist (but make sure it is up-to-date).
---
 .gitignore | 1 +
 1 file changed, 1 insertion(+)

(limited to '.gitignore')

diff --git a/.gitignore b/.gitignore
index 35cdf9b4e..64c49b008 100644
--- a/.gitignore
+++ b/.gitignore
@@ -43,6 +43,7 @@ TAGS
 .DS_Store
 .pc
 bin/
+_build_ci
 _build
 myocamlbuild_config.ml
 config/Makefile
-- 
cgit v1.2.3