Gilles Peskine d1174cf015 Fix sometimes-spurious warning about changed config.h
After backing up and restoring config.h, `git diff-files` may report
it as potentially-changed because it isn't sure whether the index is
up to date. Use `git diff` instead: it actually reads the file.
2019-01-10 18:29:15 +01:00
..
2018-08-06 11:42:56 +01:00
2016-01-12 14:48:03 +00:00
2015-04-09 10:53:11 +02:00
2015-08-04 17:46:21 +02:00
2017-05-16 17:53:03 +02:00