From 27882e4edd07e306333fdc024330982741416a19 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 24 Jul 2010 15:56:00 +0000
Subject: 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
---
 dev/header              |  2 +-
 dev/tools/change-header | 37 ++++++++++++++++++++++++++++++-------
 2 files changed, 31 insertions(+), 8 deletions(-)

(limited to 'dev')

diff --git a/dev/header b/dev/header
index 57945e47ea..d90be792d5 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 8b3560e89b..61cc866602 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
-- 
cgit v1.2.3