From cf04e49c5426da3ea684f8e545652803106af0c2 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 19 Dec 2017 15:54:34 +0100
Subject: Fix CI with parallel make (messed up dependencies)

When invoking through Makefile we always rebuild dependencies. To skip
dependencies, invoke ci-wrapper directly. We make Circle CI do this.

In order to properly support invoking ci-wrapper directly we replace
"make" in ci-common by a bash function which adds -j to the make
invocation outside submakes. We also set TIMED in the ci-wrapper.
---
 Makefile.ci | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'Makefile.ci')

diff --git a/Makefile.ci b/Makefile.ci
index 2a6222e222..334827a937 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -25,9 +25,6 @@ CI_TARGETS=ci-all \
 
 .PHONY: $(CI_TARGETS)
 
-_build_ci/.ci-%.done:
-	+./dev/ci/ci-wrapper.sh $*
-
 ci-color: ci-bignums
 
 ci-math-classes: ci-bignums
@@ -37,7 +34,8 @@ ci-corn: ci-math-classes
 ci-formal-topology: ci-corn
 
 # Generic rule, we use make to ease travis integration with mixed rules
-$(CI_TARGETS): ci-%: _build_ci/.ci-%.done
+$(CI_TARGETS): ci-%:
+	+./dev/ci/ci-wrapper.sh $*
 
 # For emacs:
 # Local Variables:
-- 
cgit v1.2.3