From d06af26e6cd93c6bb819b38573603a5e1121ed68 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 13 Jun 2017 18:24:45 +0200
Subject: Each user overlay goes into its own file.

This will avoid stupid merge conflicts in the future.
---
 dev/ci/ci-common.sh | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'dev/ci/ci-common.sh')

diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index f1e1515d41..5435e95885 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -18,7 +18,9 @@ ls "$COQBIN"
 # Where we clone and build external developments
 CI_BUILD_DIR=`pwd`/_build_ci
 
-source ${ci_dir}/ci-user-overlay.sh
+for overlay in ${ci_dir}/user-overlays/*.sh; do
+  source ${overlay}
+done
 source ${ci_dir}/ci-basic-overlay.sh
 
 mathcomp_CI_DIR=${CI_BUILD_DIR}/math-comp
-- 
cgit v1.2.3