From d5539f3c7057fb2cbb3b74a6448d02919d80dabb Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 2 Dec 2020 10:09:02 +0100
Subject: [PATCH] [dev] do not attempt to lint deleted files in pre-commit hook
---
devel_tools/git-hooks/pre-commit | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/devel_tools/git-hooks/pre-commit b/devel_tools/git-hooks/pre-commit
index d444779a231..fec935b5fc0 100755
--- a/devel_tools/git-hooks/pre-commit
+++ b/devel_tools/git-hooks/pre-commit
@@ -17,6 +17,6 @@ else
fi
MANUAL_ML_FILES=\
-$(git diff-index --name-only $against | \
+$(git diff-index --name-only --diff-filter d $against | \
grep -e '^src/.*\.mli\?$' | tr '\n' ' ') \
make ${MAKELEVEL} lint
--
GitLab