Merge branch 'fix/dev/commit-hook' into 'master'

[lint] fix identification of files that have been subject to git mv

See merge request frama-c/frama-c!3917

share/Makefile.linting

@@ -207,8 +207,12 @@ LINT.dir=$(wildcard $(LINT_DIR))
 
 ######## LINT_DIFF filter
 
+define LINT.file-list-from-git-diff-info
+$(GIT) diff --name-status $(1) | $(GREP) -v "^D" | $(SED) -e "s/^[CR][0-9]\+[ \t]\+[^ \t]\+[ \t]\+//" -e "s/^[AM][ \t]*//"
+endef
+
 define LINT.file-list-from-git-diff
-$(GIT) diff --name-status $(1) | $(GREP) -v "^D" | $(SED) "s/^.[ \t]*//" | $(TR) '\n' '\000'
+$(call LINT.file-list-from-git-diff-info,$(1)) | $(TR) '\n' '\000'
 endef
 
 define LINT.file-list-filter-with-git-diff
@@ -218,7 +222,7 @@ $$(LINT.$(1)-filter-targets):: LINT.FILE_LIST=$$(call LINT.file-list-from-git-di
 $$(LINT.$(1)-filter-targets):: %.$(1) : $(3) %
 	@echo [LINT] Done: LINT_DIFF=\"$(2)\" make $$(basename $$@)
 	@echo [LINT] checked file list:
-	$$(GIT) diff --name-status $(2)
+	$$(call LINT.file-list-from-git-diff-info,$(2))
 endef
 
 ifeq ($(LINT_DIFF),)