doc: Document that GNU tools are required for linters

This commit is contained in:
MarcoFalke 2019-10-17 10:53:21 -04:00
parent 4444704ca9
commit fadccb263b
No known key found for this signature in database
GPG key ID: CE2B75697E69A548

View file

@ -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
====================