diff options
| author | Alejandro Colomar <alx@kernel.org> | 2023-03-11 16:25:21 +0100 |
|---|---|---|
| committer | Alejandro Colomar <alx@kernel.org> | 2023-03-11 16:25:21 +0100 |
| commit | b4c10c038e103c04b4ed1e7446fd2f161e75eaf5 (patch) | |
| tree | a8e9b7576909374c4bc0e7d269c77a0b38a95682 | |
| parent | 702b8bf597504e3860740209cc98827ab6830764 (diff) | |
| download | man-pages-b4c10c038e103c04b4ed1e7446fd2f161e75eaf5.tar.gz | |
CONTRIBUTING: Use make(1)'s '-t' to avoid linting everything
Suggested-by: Paul Smith <psmith@gnu.org>
Cc: Dmitry Goncharov <dgoncharov@users.sf.net>
Signed-off-by: Alejandro Colomar <alx@kernel.org>
| -rw-r--r-- | CONTRIBUTING | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/CONTRIBUTING b/CONTRIBUTING index 45bc86a28a..e20447ffa8 100644 --- a/CONTRIBUTING +++ b/CONTRIBUTING @@ -135,12 +135,10 @@ Description new warnings. However, you might still get warnings that are not your fault. To minimize that, do the following steps: - (1) Lint first all of the pages, so that make(1) knows that it only - needs to lint again pages that you will touch. This example is - shown with '-j' because it would take a long time (around a couple - of minutes) to run without parallel execution. + (1) First use make(1)'s -t option, so that make(1) knows that it only + needs to lint again pages that you will touch. - $ make -ij lint >/dev/null 2>&1 + $ make -t lint (2) Touch the page that you'll edit, and run make(1) again, to see which warnings you'll still see from that page that are not your |