aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rw-r--r--dev/header.c2
-rw-r--r--dev/header.ml2
-rw-r--r--dev/header.py2
-rwxr-xr-xdev/tools/change-header21
-rw-r--r--dev/top_printers.ml2
-rw-r--r--dev/top_printers.mli2
6 files changed, 14 insertions, 17 deletions
diff --git a/dev/header.c b/dev/header.c
index 663c43b3d6..6201cb3b73 100644
--- a/dev/header.c
+++ b/dev/header.c
@@ -1,6 +1,6 @@
/************************************************************************/
/* * The Coq Proof Assistant / The Coq Development Team */
-/* v * INRIA, CNRS and contributors - Copyright 1999-2018 */
+/* v * INRIA, CNRS and contributors - Copyright 1999-2019 */
/* <O___,, * (see CREDITS file for the list of authors) */
/* \VV/ **************************************************************/
/* // * This file is distributed under the terms of the */
diff --git a/dev/header.ml b/dev/header.ml
index 7c3ee60040..87553dcb56 100644
--- a/dev/header.ml
+++ b/dev/header.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/dev/header.py b/dev/header.py
index f81c8aa6a2..86114503d4 100644
--- a/dev/header.py
+++ b/dev/header.py
@@ -1,6 +1,6 @@
##########################################################################
## # The Coq Proof Assistant / The Coq Development Team ##
-## v # INRIA, CNRS and contributors - Copyright 1999-2018 ##
+## v # INRIA, CNRS and contributors - Copyright 1999-2019 ##
## <O___,, # (see CREDITS file for the list of authors) ##
## \VV/ ###############################################################
## // # This file is distributed under the terms of the ##
diff --git a/dev/tools/change-header b/dev/tools/change-header
index 687c02f4f1..59c6f43958 100755
--- a/dev/tools/change-header
+++ b/dev/tools/change-header
@@ -13,22 +13,19 @@ newheader=$2
if [ ! -f $oldheader ]; then echo Cannot read file $oldheader; exit 1; fi
if [ ! -f $newheader ]; then echo Cannot read file $newheader; exit 1; fi
-n=`wc -l $oldheader | sed -e "s/ *\([0-9]*\).*/\1/g"`
-nsucc=`expr $n + 1`
-
-linea='(* -*- coding:utf-8 -*- *)'
-lineb='(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)'
+n=$(wc -l $oldheader | sed -e "s/ *\([0-9]*\).*/\1/g")
+nsucc=$(expr $n + 1)
modified=0
kept=0
-for i in `find . -name \*.mli -o -name \*.ml -o -name \*.mlg -o -name \*.mll -o -name \*.mly -o -name \*.mlp -o -name \*.v`; do
- headline=`head -n 1 $i`
- if `echo $headline | grep "(\* -\*- .* \*)" > /dev/null`; then
- # Has emacs header
+for i in $(git grep --name-only --fixed-strings "$(head -1 $oldheader)"); do
+ headline=$(head -n 1 $i)
+ if $(echo $headline | grep "(\* -\*- .* \*)" > /dev/null) || $(echo $headline | grep "^#\!" > /dev/null); then
+ # Has header
head -n +$nsucc $i | tail -n $n > $i.head.tmp$$
hasheadline=1
- nnext=`expr $nsucc + 1`
+ nnext=$(expr $nsucc + 1)
else
head -n +$n $i > $i.head.tmp$$
hasheadline=0
@@ -44,9 +41,9 @@ for i in `find . -name \*.mli -o -name \*.ml -o -name \*.mlg -o -name \*.mll -o
cat $newheader >> $i.tmp$$
tail -n +$nnext $i >> $i.tmp$$
mv $i.tmp$$ $i
- modified=`expr $modified + 1`
+ modified=$(expr $modified + 1)
else
- kept=`expr $kept + 1`
+ kept=$(expr $kept + 1)
fi
rm $i.head.tmp$$
done
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 87b4d31054..8343853af5 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/dev/top_printers.mli b/dev/top_printers.mli
index 2aa1808322..5a2144f996 100644
--- a/dev/top_printers.mli
+++ b/dev/top_printers.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)