aboutsummaryrefslogtreecommitdiff
path: root/Makefile.ci
diff options
context:
space:
mode:
authorMaxime Dénès2018-03-05 13:30:08 +0100
committerMaxime Dénès2018-03-05 13:30:08 +0100
commit15331729aaab16678c2f7e29dd391f72df53d76e (patch)
tree259c87baa8152c7b67fd339bb90f5ecf6317c207 /Makefile.ci
parent736e86e06b5831a0dd4b6a655708b4ffd2b4ee64 (diff)
parent629fbc743f8b5e7623a6834f19885b2e379cb782 (diff)
Merge PR #6855: Update headers following #6543.
Diffstat (limited to 'Makefile.ci')
-rw-r--r--Makefile.ci10
1 files changed, 10 insertions, 0 deletions
diff --git a/Makefile.ci b/Makefile.ci
index 4e92264d62..3c26bf964b 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -1,3 +1,13 @@
+##########################################################################
+## # The Coq Proof Assistant / The Coq Development Team ##
+## v # INRIA, CNRS and contributors - Copyright 1999-2018 ##
+## <O___,, # (see CREDITS file for the list of authors) ##
+## \VV/ ###############################################################
+## // # This file is distributed under the terms of the ##
+## # GNU Lesser General Public License Version 2.1 ##
+## # (see LICENSE file for the text of the license) ##
+##########################################################################
+
CI_TARGETS=ci-bignums \
ci-color \
ci-compcert \