diff options
Diffstat (limited to 'dev/tools/change-header')
| -rwxr-xr-x | dev/tools/change-header | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/dev/tools/change-header b/dev/tools/change-header index 59c6f43958..3b0a9d1ef9 100755 --- a/dev/tools/change-header +++ b/dev/tools/change-header @@ -43,6 +43,7 @@ for i in $(git grep --name-only --fixed-strings "$(head -1 $oldheader)"); do mv $i.tmp$$ $i modified=$(expr $modified + 1) else + echo "$i: header unchanged" kept=$(expr $kept + 1) fi rm $i.head.tmp$$ |