Mention what file has changed

This commit is contained in:
rl1987 2019-03-06 19:42:29 +02:00
parent 73fed3ee1c
commit 7b5f31f2d6

View File

@ -28,7 +28,11 @@ check_for_diffs() {
check_for_script_update() { check_for_script_update() {
fullpath="$git_toplevel/scripts/maint/$1" fullpath="$git_toplevel/scripts/maint/$1"
git diff ORIG_HEAD HEAD --exit-code -- "$fullpath" if ! git diff ORIG_HEAD HEAD --exit-code -- "$fullpath" >/dev/null
then
echo "ATTENTION: $1 has changed:"
git diff ORIG_HEAD HEAD -- "$fullpath"
fi
} }
check_for_diffs "pre-push" check_for_diffs "pre-push"