From 37e3bf2676cb7ca28a8908cae0d7e2d4f410ffd8 Mon Sep 17 00:00:00 2001
From: Hendrik van Antwerpen <hendrikvanantwerpen@github.com>
Date: Mon, 1 Nov 2021 14:39:33 +0100
Subject: [PATCH] Fix incorrect file changes being reported

---
 script/check-generated-files | 16 +++++++++++-----
 1 file changed, 11 insertions(+), 5 deletions(-)

diff --git a/script/check-generated-files b/script/check-generated-files
index dff20d01a..c1f216dde 100755
--- a/script/check-generated-files
+++ b/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