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.contrib | 13 +++++++++++++
 1 file changed, 13 insertions(+)
 create mode 100644 Makefile.contrib

(limited to 'Makefile.contrib')

diff --git a/Makefile.contrib b/Makefile.contrib
new file mode 100644
index 0000000000..2e3ed94c53
--- /dev/null
+++ b/Makefile.contrib
@@ -0,0 +1,13 @@
+.PHONY: contrib-all contrib-hott contrib-math-comp
+
+contrib-all: contrib-hott contrib-math-comp
+
+# TODO Do generic rule
+contrib-hott:
+	./tools/ci/contrib-hott.sh
+
+contrib-math-comp:
+	./tools/ci/contrib-math-comp.sh
+
+contrib-compcert:
+	./tools/ci/contrib-compcert.sh
-- 
cgit v1.2.3