Fix incorrect file changes being reported

script/check-generated-files

@@ -2,11 +2,17 @@
 
 set -eu
 
-if ! git diff-index --quiet HEAD -- {tsx,typescript}/src/; then
-    cat 1>&2 <<EOF
-Generated files in the working tree are inconsistent with HEAD.
-Make sure to commit generated files in {tsx,typescript}/src/ when the grammar changes.
-EOF
+## Update index to make sure the subsequent diff-index command only reports
+## a change if the file content actually changed. Not updating the index can
+## give incorrect results when this script is run right after a build.
+
+git update-index -q --really-refresh
+
+if ! git diff-index --exit-code --name-status HEAD -- {tsx,typescript}/src/; then
+    echo "The following files are not up to date in the repository:" 1>&2
+    git diff-index --name-status HEAD 1>&2
+    echo "Run a build and commit the generated files to resolve this issue." 1>&2
+    git diff-index -p HEAD
     exit 1
 fi