aboutsummaryrefslogtreecommitdiff
path: root/dev/header.c
diff options
context:
space:
mode:
authorHugo Herbelin2020-03-18 17:32:36 +0100
committerHugo Herbelin2020-03-18 17:32:36 +0100
commitfb7292570380e0490d7c74db1718725149996ffd (patch)
tree2ca0a82017f81300e1e48ce9b06ab50e05d681e4 /dev/header.c
parent55490662517966d01a53ddd708709d1fc739286c (diff)
parenta99776e10e0b2198d2b811ad82631111fb450f8a (diff)
Merge PR #11559: Remove year in headers.
Reviewed-by: jfehrle
Diffstat (limited to 'dev/header.c')
-rw-r--r--dev/header.c4
1 files changed, 2 insertions, 2 deletions
diff --git a/dev/header.c b/dev/header.c
index 6201cb3b73..f31efcba47 100644
--- a/dev/header.c
+++ b/dev/header.c
@@ -1,7 +1,7 @@
/************************************************************************/
/* * The Coq Proof Assistant / The Coq Development Team */
-/* v * INRIA, CNRS and contributors - Copyright 1999-2019 */
-/* <O___,, * (see CREDITS file for the list of authors) */
+/* v * Copyright INRIA, CNRS and contributors */
+/* <O___,, * (see version control and CREDITS file for authors & dates) */
/* \VV/ **************************************************************/
/* // * This file is distributed under the terms of the */
/* * GNU Lesser General Public License Version 2.1 */