tree 1fcc2aee19454810ceb4e99289f682bb7382428a
parent c70637a5f01cfa15353161f4c092091635c89c5a
author Gilles Peskine <Gilles.Peskine@arm.com> 1547069401 +0100
committer Gilles Peskine <Gilles.Peskine@arm.com> 1547141355 +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.