diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-22 06:31:30 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-22 06:31:30 +0000 |
commit | d6c87f235a98c05a26b4a0e87129335d034219af (patch) | |
tree | 0cdbf9db7dc808621befc220892b9b7e083cdfe0 /dev/tools | |
parent | a1f06f016be512c21cb475491ec9924eea7ff288 (diff) |
New script dev/tools/change-header to automatically update Coq files headers.
Applied it to fix mli file headers.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13176 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/tools')
-rwxr-xr-x | dev/tools/change-header | 32 |
1 files changed, 32 insertions, 0 deletions
diff --git a/dev/tools/change-header b/dev/tools/change-header new file mode 100755 index 000000000..8b3560e89 --- /dev/null +++ b/dev/tools/change-header @@ -0,0 +1,32 @@ +#!/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` + +filter="-name \*.mli -o -name \*.ml -o -name \*.ml4 -o -name \*.mll -o -name \*.mly" + +for i in `find . $filter`; do + head -n +$n $i > $i.head.tmp$$ + 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$$ + mv $i.tmp$$ $i + else + echo "$i: old header not found, file untouched" + fi +done |