aboutsummaryrefslogtreecommitdiff
path: root/dev/tools
diff options
context:
space:
mode:
authorGaëtan Gilbert2020-03-30 18:32:29 +0200
committerGaëtan Gilbert2020-03-30 18:44:21 +0200
commit2e3621d91f0306dbc9f0b576cd2f839e66390c42 (patch)
tree0bd787aee69ff63a57df5f8a63762d5790e382e4 /dev/tools
parentd2f21a119fea99d8621fb227b82fa8a1bf17d9fb (diff)
Fix commit hook when there are no changes (eg amend message)
Fix #11967
Diffstat (limited to 'dev/tools')
-rwxr-xr-xdev/tools/pre-commit45
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.)"