tree bcd6f038f02ed850279b64604a184182c252000f
parent 92bff7f9bfbcb6b95ab3975afccd5a6afee8f72a
author Gilles Peskine <Gilles.Peskine@arm.com> 1547069401 +0100
committer Gilles Peskine <Gilles.Peskine@arm.com> 1547141780 +0100

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.