Dirk Mueller 958b700317 Use git grep -h for skipping the filenames
That seems to be more portable accross different environments
(aka make it work for dirk)

Change-Id: I4eee201ed0114cf7aa9f9be39d1335326691bf99
2017-02-21 16:19:54 +01:00
..
2016-04-24 17:21:18 -05:00
2016-12-19 07:13:35 +00:00