tree 826de8a42e4342a7d16d5836e20a34226da54f9f
parent 2906a0ae8a112b3edd9d857e7ed8bec52fceb7f8
author Gilles Peskine <Gilles.Peskine@arm.com> 1547069401 +0100
committer Gilles Peskine <Gilles.Peskine@arm.com> 1547141377 +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. To avoid this, make sure that the git index is up-to-date.

This fixes the warning about changed config.h that you might get when
you run all.sh twice in succession, yet if you run `git status` or
`git diff` everything seems up to date and you no longer get the
warning because these git commands update the index.

https://stackoverflow.com/questions/36367190/git-diff-files-output-changes-after-git-status