Quelle  change-header   Sprache: unbekannt

#!/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)

modified=0
kept=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