1 files changed, 55 insertions, 0 deletions
diff --git a/dev/tools/change-header b/dev/tools/change-header
new file mode 100755
index 00000000..61cc8666
--- /dev/null
+++ b/dev/tools/change-header
@@ -0,0 +1,55 @@
+#!/bin/sh
+
+#This script changes the header of .ml* files
+
+if [ ! $# = 2 ]; then
+  echo Usage: change-header old-header-file new-header-file
+  exit 1
+fi
+
+oldheader=$1
+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" -*- *)'
+
+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
+    echo "$i: header changed"
+    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
+    kept=`expr $kept + 1`
+  fi
+  rm $i.head.tmp$$
+done
+
+echo $modified files updated 
+echo $kept files unchanged