diff options
Diffstat (limited to 'Makefile')
-rw-r--r-- | Makefile | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -246,9 +246,9 @@ devdocclean: rm -f $(OCAMLDOCDIR)/html/*.html ########################################################################### -# Contrib tests +# Continuous Intregration Tests ########################################################################### -include Makefile.contrib +include Makefile.ci ########################################################################### # Emacs tags |