diff options
| author | Gaëtan Gilbert | 2020-03-30 18:32:29 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-03-30 18:44:21 +0200 |
| commit | 2e3621d91f0306dbc9f0b576cd2f839e66390c42 (patch) | |
| tree | 0bd787aee69ff63a57df5f8a63762d5790e382e4 /dev/tools | |
| parent | d2f21a119fea99d8621fb227b82fa8a1bf17d9fb (diff) | |
Fix commit hook when there are no changes (eg amend message)
Fix #11967
Diffstat (limited to 'dev/tools')
| -rwxr-xr-x | dev/tools/pre-commit | 45 |
1 files changed, 22 insertions, 23 deletions
diff --git a/dev/tools/pre-commit b/dev/tools/pre-commit index 9620e7bc8c..633913aac6 100755 --- a/dev/tools/pre-commit +++ b/dev/tools/pre-commit @@ -33,44 +33,43 @@ git diff-index -p HEAD > "$tree" # reset work tree and index # NB: untracked files which were not added are untouched -git apply --whitespace=nowarn --cached -R "$index" -git apply --whitespace=nowarn -R "$tree" +if [ -s "$index" ]; then git apply --whitespace=nowarn --cached -R "$index"; fi +if [ -s "$tree" ]; then git apply --whitespace=nowarn -R "$tree"; fi # Fix index # For end of file newlines we must go through the worktree -1>&2 echo "Fixing staged changes..." -git apply --cached --whitespace=fix "$index" -git apply --whitespace=fix "$index" 2>/dev/null # no need to repeat yourself -git diff --cached --name-only -z | xargs -0 dev/tools/check-eof-newline.sh --fix -git diff --cached --name-only -z | grep -E '.*\.mli?$' -z | xargs -0 "$ocamlformat" -i || true -git add -u -1>&2 echo #newline +if [ -s "$index" ]; then + 1>&2 echo "Fixing staged changes..." + git apply --cached --whitespace=fix "$index" + git apply --whitespace=fix "$index" 2>/dev/null # no need to repeat yourself + git diff --cached --name-only -z | xargs -0 dev/tools/check-eof-newline.sh --fix + git diff --cached --name-only -z | grep -E '.*\.mli?$' -z | xargs -0 "$ocamlformat" -i || true + git add -u + 1>&2 echo #newline +fi # reset work tree git diff-index -p --cached HEAD > "$fixed_index" # If all changes were bad whitespace changes the patch is empty # making git fail. Don't fail now: we fix the worktree first. -if [ -s "$fixed_index" ] -then - git apply --whitespace=nowarn -R "$fixed_index" -fi +if [ -s "$fixed_index" ]; then git apply --whitespace=nowarn -R "$fixed_index"; fi # Fix worktree -1>&2 echo "Fixing unstaged changes..." -git apply --whitespace=fix "$tree" -git diff --name-only -z | xargs -0 dev/tools/check-eof-newline.sh --fix -git diff --name-only -z | grep -E '.*\.mli?$' -z | xargs -0 "$ocamlformat" -i || true -1>&2 echo #newline +if [ -s "$tree" ]; then + 1>&2 echo "Fixing unstaged changes..." + git apply --whitespace=fix "$tree" + git diff --name-only -z | xargs -0 dev/tools/check-eof-newline.sh --fix + git diff --name-only -z | grep -E '.*\.mli?$' -z | xargs -0 "$ocamlformat" -i || true + 1>&2 echo #newline +fi -if ! [ -s "$fixed_index" ] -then - 1>&2 echo "No changes after fixing whitespace and formatting issues!" +if [ -s "$index" ] && ! [ -s "$fixed_index" ]; then + 1>&2 echo "Fixing whitespace and formatting issues cancelled all changes." exit 1 fi # Check that we did fix whitespace -if ! git diff-index --check --cached HEAD; -then +if ! git diff-index --check --cached HEAD; then 1>&2 echo "Auto-fixing whitespace failed: errors remain." 1>&2 echo "This may fix itself if you try again." 1>&2 echo "(Consider whether the number of errors decreases after each run.)" |
