X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=build-aux%2Fgit-version-gen;h=e754c77d6a383a03a16e42d6c83f4b7af4ced227;hb=197b47e41bbf202b2f1abf45a43515200470bf47;hp=16da2a8f6c9aa4b0c7c9c85af00fe2bbd1de6531;hpb=c9f911dbdb52770946a6e93d283caa0583ade4a5;p=pspp

diff --git a/build-aux/git-version-gen b/build-aux/git-version-gen
index 16da2a8f6c..e754c77d6a 100755
--- a/build-aux/git-version-gen
+++ b/build-aux/git-version-gen
@@ -127,7 +127,7 @@ fi
 v=`echo "$v" |sed 's/^v//'`
 
 # Don't declare a version "dirty" merely because a time stamp has changed.
-git status > /dev/null 2>&1
+git update-index --refresh > /dev/null 2>&1
 
 dirty=`sh -c 'git diff-index --name-only HEAD' 2>/dev/null` || dirty=
 case "$dirty" in