aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-07-24 15:56:00 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-07-24 15:56:00 +0000
commit27882e4edd07e306333fdc024330982741416a19 (patch)
tree0d91a4d3d9f8a6ef94dc1a6fc818dec997bd4750 /dev
parent657f394cf6de00d852bf33ea8d7f17f1daededbf (diff)
Updated COPYRIGHT file and header. Improved and fixed header updater.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13322 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
-rw-r--r--dev/header2
-rwxr-xr-xdev/tools/change-header37
2 files changed, 31 insertions, 8 deletions
diff --git a/dev/header b/dev/header
index 57945e47e..d90be792d 100644
--- a/dev/header
+++ b/dev/header
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/dev/tools/change-header b/dev/tools/change-header
index 8b3560e89..61cc86660 100755
--- a/dev/tools/change-header
+++ b/dev/tools/change-header
@@ -16,17 +16,40 @@ 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`
-filter="-name \*.mli -o -name \*.ml -o -name \*.ml4 -o -name \*.mll -o -name \*.mly"
+linea='(* -*- coding:utf-8 -*- *)'
+lineb='(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)'
-for i in `find . $filter`; do
- head -n +$n $i > $i.head.tmp$$
+modified=0
+kept=0
+
+for i in `find . -name \*.mli -o -name \*.ml -o -name \*.ml4 -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
+ head -n +$nsucc $i | tail -n $n > $i.head.tmp$$
+ hasheadline=1
+ nnext=`expr $nsucc + 1`
+ else
+ head -n +$n $i > $i.head.tmp$$
+ hasheadline=0
+ nnext=$nsucc
+ fi
if diff -a -q $oldheader $i.head.tmp$$ > /dev/null; then
- rm $i.head.tmp$$
echo "$i: header changed"
- cat dev/header > $i.tmp$$
- tail -n +$nsucc $i >> $i.tmp$$
+ if [ $hasheadline = 1 ]; then
+ echo $headline > $i.tmp$$
+ else
+ touch $i.tmp$$
+ fi
+ cat $newheader >> $i.tmp$$
+ tail -n +$nnext $i >> $i.tmp$$
mv $i.tmp$$ $i
+ modified=`expr $modified + 1`
else
- echo "$i: old header not found, file untouched"
+ kept=`expr $kept + 1`
fi
+ rm $i.head.tmp$$
done
+
+echo $modified files updated
+echo $kept files unchanged