From 2e3621d91f0306dbc9f0b576cd2f839e66390c42 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 30 Mar 2020 18:32:29 +0200
Subject: Fix commit hook when there are no changes (eg amend message)

Fix #11967
---
 dev/tools/pre-commit | 45 ++++++++++++++++++++++-----------------------
 1 file changed, 22 insertions(+), 23 deletions(-)

(limited to 'dev/tools')

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.)"
-- 
cgit v1.2.3