diff options
| author | MarcoFalke <falke.marco@gmail.com> | 2019-10-17 10:53:21 -0400 |
|---|---|---|
| committer | MarcoFalke <falke.marco@gmail.com> | 2019-10-17 10:52:11 -0400 |
| commit | fadccb263baf6b8694f750623add42f966e423a3 (patch) | |
| tree | 259110142936ccb30b8b980e11650a48719e6f96 | |
| parent | 4444704ca9f66cdc24ab2d444941354db1dfed06 (diff) | |
doc: Document that GNU tools are required for linters
| -rw-r--r-- | test/lint/README.md | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/test/lint/README.md b/test/lint/README.md index 15974a3598..f415d619ee 100644 --- a/test/lint/README.md +++ b/test/lint/README.md @@ -7,6 +7,8 @@ Check for missing documentation of command line options. commit-script-check.sh ====================== Verification of [scripted diffs](/doc/developer-notes.md#scripted-diffs). +Scripted diffs are only assumed to run on the latest LTS release of Ubuntu. Running them on other operating systems +might require installing GNU tools, such as GNU sed. git-subtree-check.sh ==================== |