From a33323d54cf78762f7ba1afc39a2f5a5ddb67a57 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 18 Mar 2020 11:49:42 +0100
Subject: Also show unchanged headers.

---
 dev/tools/change-header | 1 +
 1 file changed, 1 insertion(+)

(limited to 'dev/tools')

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$$
-- 
cgit v1.2.3