From 7aa2c39387a9781bf406c763c538859f24b8b7f3 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 5 Dec 2016 10:58:04 +0100
Subject: Compute dependency of C files only in kernel/byterun.

Some C files included in build scripts (in dev/build) were triggering
errors or warnings on non-win32 platforms.

Note that ide/ide_win32_stubs.c was already handled through an ad-hoc
rule in Makefile.

If you add a new C file outside of kernel/byterun, please extend the CFILES
variable.
---
 Makefile | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 6649542c88..1dd4efca2e 100644
--- a/Makefile
+++ b/Makefile
@@ -59,6 +59,10 @@ define find
  $(shell find . $(FIND_VCS_CLAUSE) '(' -name $(1) ')' -print | sed 's|^\./||')
 endef
 
+define findindir
+ $(shell find $(1) $(FIND_VCS_CLAUSE) '(' -name $(2) ')' -print | sed 's|^\./||')
+endef
+
 define findx
  $(shell find . $(FIND_VCS_CLAUSE) '(' -name $(1) ')' -exec $(2) {} \; | sed 's|^\./||')
 endef
@@ -68,7 +72,7 @@ endef
 LEXFILES := $(call find, '*.mll')
 export MLLIBFILES := $(call find, '*.mllib') $(call find, '*.mlpack')
 export ML4FILES := $(call find, '*.ml4')
-export CFILES := $(call find, '*.c')
+export CFILES := $(call findindir, 'kernel/byterun', '*.c')
 
 # NB: The lists of currently existing .ml and .mli files will change
 # before and after a build or a make clean. Hence we do not export
-- 
cgit v1.2.3


From 3e07baa69f1e7de02670dd20dd7577d70c2f2653 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 4 Feb 2017 21:25:14 +0100
Subject: [travis] [External CI] compcert HoTT math-comp

- Improve the setup to support external contribs.
  We use a more minimalistic Coq build, gaining a few extra minutes.
- [math-comp] workaround `make -j` bug to enable parallel building.
---
 Makefile | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 0f9619c01b..25a97f9bb1 100644
--- a/Makefile
+++ b/Makefile
@@ -245,6 +245,11 @@ devdocclean:
 	rm -f $(OCAMLDOCDIR)/ocamldoc.sty $(OCAMLDOCDIR)/coq.tex 
 	rm -f $(OCAMLDOCDIR)/html/*.html
 
+###########################################################################
+# Contrib tests
+###########################################################################
+include Makefile.contrib
+
 ###########################################################################
 # Emacs tags
 ###########################################################################
-- 
cgit v1.2.3


From 138a4da7f0133d7b4ea06cfbc938d23ddb88c97d Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 4 Feb 2017 23:55:24 +0100
Subject: [travis] [External CI] Script renaming.

---
 Makefile | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 25a97f9bb1..e1d6e8e1d2 100644
--- a/Makefile
+++ b/Makefile
@@ -246,9 +246,9 @@ devdocclean:
 	rm -f $(OCAMLDOCDIR)/html/*.html
 
 ###########################################################################
-# Contrib tests
+# Continuous Intregration Tests
 ###########################################################################
-include Makefile.contrib
+include Makefile.ci
 
 ###########################################################################
 # Emacs tags
-- 
cgit v1.2.3