Philip Oakley <philipoakley@iee.email> writes: >> 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.