From 1515c199a47ff11b2016067ac031bce7209150dc Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 8 Oct 2020 18:35:36 +0200
Subject: [PATCH] [Makefile] Allow pre-commit hook to define precisely what it
 wants to lint

---
 Makefile | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/Makefile b/Makefile
index 647c9af3991..425f7548150 100644
--- a/Makefile
+++ b/Makefile
@@ -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+=ptests/ptests.ml
+
+ifeq ($(origin MANUAL_ML_FILES),undefined)
 MANUAL_ML_FILES:=$(filter-out $(GENERATED) $(PLUGIN_GENERATED_LIST), $(ALL_ML_FILES))
+endif
 
 # Allow control of files to be linted/fixed by external sources
 # (e.g. pre-commit hook that will concentrate on files which have changed)
-- 
GitLab