mirror of https://github.com/llvm/torch-mlir
Add `--no-index` to CI's git-diff check on generated files (#1428)
`git diff` does not work by default on untracked files. Since the function `_check_file_not_changed_by` stores the new generated file in an untracked file, `git diff` was not catching any modifications in the new generated file. This commit adds the flag `--no-index` to make `git diff` work with untracked files.pull/1438/head
parent
e193e4b9be
commit
2509641cab
|
@ -211,12 +211,12 @@ function _check_file_not_changed_by() {
|
||||||
mv "$file_backup" "$file"
|
mv "$file_backup" "$file"
|
||||||
# We use git-diff as "just a diff program" (no SCM stuff) because it has
|
# We use git-diff as "just a diff program" (no SCM stuff) because it has
|
||||||
# nicer output than regular `diff`.
|
# nicer output than regular `diff`.
|
||||||
if ! git diff --quiet "$file" "$file_new"; then
|
if ! git diff --no-index --quiet "$file" "$file_new"; then
|
||||||
echo "#######################################################"
|
echo "#######################################################"
|
||||||
echo "Generated file '${file}' is not up to date (see diff below)"
|
echo "Generated file '${file}' is not up to date (see diff below)"
|
||||||
echo ">>> Please run '${cmd}' to update it <<<"
|
echo ">>> Please run '${cmd}' to update it <<<"
|
||||||
echo "#######################################################"
|
echo "#######################################################"
|
||||||
git diff --color=always "$file" "$file_new"
|
git diff --no-index --color=always "$file" "$file_new"
|
||||||
# TODO: Is there a better cleanup strategy that doesn't require duplicating
|
# TODO: Is there a better cleanup strategy that doesn't require duplicating
|
||||||
# this inside and outside the `if`?
|
# this inside and outside the `if`?
|
||||||
rm "$file_new"
|
rm "$file_new"
|
||||||
|
|
Loading…
Reference in New Issue