Also show unchanged headers.

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$$