Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354#!/bin/sh
#This script changes the header of .ml* files
if [ ! $# = 2 ]; then echo Usage: change-header old-header-file new-header-file exit 1fi
oldheader=$1newheader=$2
if [ ! -f $oldheader ]; then echo Cannot read file $oldheader; exit 1; fiif [ ! -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)
modified=0kept=0
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) 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 echo "$i: header unchanged" kept=$(expr $kept + 1) fi rm $i.head.tmp$$done
echo $modified files updated echo $kept files unchanged