Skip to content

GitLab

Commit 1515c199 authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

[Makefile] Allow pre-commit hook to define precisely what it wants to lint

parent 09d4f920
Hide whitespace changes
Inline Side-by-side
Makefile
View file @ 1515c199
...@@ -1708,7 +1708,10 @@ check-devguide: $(CHECK_CODE) $(DOC_DEPEND) $(DOC_DIR)/kernel-doc.ocamldoc ...@@ -1708,7 +1708,10 @@ check-devguide: $(CHECK_CODE) $(DOC_DEPEND) $(DOC_DIR)/kernel-doc.ocamldoc
ALL_ML_FILES:=$(shell find src -name '*.ml' -print -o -name '*.mli' -print -o -path '*/tests' -prune '!' -name '*') ALL_ML_FILES:=$(shell find src -name '*.ml' -print -o -name '*.mli' -print -o -path '*/tests' -prune '!' -name '*')
ALL_ML_FILES+=ptests/ptests.ml ALL_ML_FILES+=ptests/ptests.ml
ifeq ($(origin MANUAL_ML_FILES),undefined)
MANUAL_ML_FILES:=$(filter-out $(GENERATED) $(PLUGIN_GENERATED_LIST), $(ALL_ML_FILES)) MANUAL_ML_FILES:=$(filter-out $(GENERATED) $(PLUGIN_GENERATED_LIST), $(ALL_ML_FILES))
endif
# Allow control of files to be linted/fixed by external sources # Allow control of files to be linted/fixed by external sources
# (e.g. pre-commit hook that will concentrate on files which have changed) # (e.g. pre-commit hook that will concentrate on files which have changed)
......
Markdown is supported
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