diff --git a/devel_tools/git-hooks/pre-commit b/devel_tools/git-hooks/pre-commit
index d444779a23156ab969227415792b622e0c9766a1..fec935b5fc0ca5d771f4b43bbd2a137789f76287 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