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

(limited to 'Makefile.contrib')

diff --git a/Makefile.contrib b/Makefile.contrib
deleted file mode 100644
index 2e3ed94c53..0000000000
--- a/Makefile.contrib
+++ /dev/null
@@ -1,13 +0,0 @@
-.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