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 25a97f9bb..e1d6e8e1d 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