Commit 259339c7 authored by Patrick Baudin's avatar Patrick Baudin
Browse files

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

Take into account more git statuses in commit hook linter

See merge request frama-c/frama-c!3912
parents 3401447d 1db8374f
......@@ -206,8 +206,12 @@ else
ifneq ($(HDRCK.HAS_GIT),)
define HDRCK.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]*//"
define HDRCK.file-list-from-git-diff
$(GIT) diff --name-status $(1) | $(GREP) -v "^D" | $(SED) "s/^.[ \t]*//" | $(TR) '\n' '\000' | $(HDRCK.FILE_ATTR)
$(call HDRCK.file-list-from-git-diff-info,$(1)) | $(TR) '\n' '\000' | $(HDRCK.FILE_ATTR)
HDRCK.main-targets=check-headers headers
......@@ -218,7 +222,7 @@ $$(HDRCK.$(1)-filter-targets):: HDRCK.SPEC=$$(call HDRCK.file-list-from-git-diff
$$(HDRCK.$(1)-filter-targets):: %.$(1) : $(3) %
@echo [HDRCK] Done: HDRCK_DIFF=\"$(2)\" make $$(basename $$@)
@echo [HDRCK] checked file list:
$$(GIT) diff --name-status $(2)
$$(call HDRCK.file-list-from-git-diff-info,$(2))
ifneq ($(HEADER_DIFF),)
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment