Merge branch 'bugfix/patrick/make-linting-without-git' into 'master'

[Makefile] Removes some warning for non git repository

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

share/Makefile.linting

@@ -168,6 +168,7 @@ ifneq ($(LINT.HAS_GIT),true)
 lint:
 	echo "'make lint' requires a git repository but, that is not"
 	echo "the case for example with 'make LINT_FILE=<file> check-syntax'"
+	git rev-parse --is-inside-work-tree
 
 else
 
@@ -205,6 +206,8 @@ ifeq ($(LINT_FILE),) ############# No lint file given
 ######## LINT_DIR filter
 LINT.dir=$(wildcard $(LINT_DIR))
 
+ifeq ($(LINT.HAS_GIT),true)  ############# For Git repository
+
 ######## LINT_DIFF filter
 
 define LINT.file-list-from-git-diff-info
@@ -314,6 +317,7 @@ $(LINT.fix-targets):
         | $(LINT.FILTER_FILE_ATTR) \
         | $(XARGS) -0 -IXX sh -c '$(LINT.make) LINT_FILE="XX" $@ || exit 255'
 
+endif ############  For Git repository
 
 else #############  LINT_FILE are given