diff --git a/FTagDumper/grid/grid-submit b/FTagDumper/grid/grid-submit index 6d07e4b732d97643f679658159c1d011fe41c3b5..abb9576953907daa8f9663e198e5556d1a0aa969 100755 --- a/FTagDumper/grid/grid-submit +++ b/FTagDumper/grid/grid-submit @@ -226,6 +226,9 @@ fi # check for uncontrolled changes if [[ ! $FORCE ]]; then + # without refreshing first, diff-index might report changes, even + # though it's only timestamps and not actual file content + git -C ${BASE} update-index --refresh if ! git -C ${BASE} diff-index --quiet HEAD; then echo "ERROR: uncommitted changes, please commit them" >&2; exit 1 fi