Re: [PATCH 4/5] doc lint: fix bugs in, simplify and improve lint script

Philip Oakley [off-list ref] writes:

quoted

diff --git a/Documentation/Makefile b/Documentation/Makefile
index 7313956d73f..6bfd8c75772 100644
--- a/Documentation/Makefile
+++ b/Documentation/Makefile

@@ -4,6 +4,7 @@ MAN5_TXT =
 MAN7_TXT =
 HOWTO_TXT =
 INCLUDE_TARGETS_TXT =
+ALL_TXT =

Maybe LINT_TXT would better clarify its use, rather than squatting on
the generic "ALL"?

As long as it is truly "all the .txt files" and will stay that way,
and the set of files we lint happens to be "everything under the sun",
I am OK to have this as ALL_TXT.  We may in the future want to do
something other than running lint-foo scripts to all the .txt files.