diff options
| author | Klaus Aehlig <klaus.aehlig@huawei.com> | 2024-08-14 16:18:55 +0200 |
|---|---|---|
| committer | Klaus Aehlig <klaus.aehlig@huawei.com> | 2024-08-20 16:39:41 +0200 |
| commit | c5d844c7c3d6f2ec8941e7b3b266775af728c2dc (patch) | |
| tree | b3fafd9bc93f489b91376ea07c788111327ca893 | |
| parent | 7482b4b90b376cc1d1d64ef827d9014879f0ef84 (diff) | |
| download | justbuild-c5d844c7c3d6f2ec8941e7b3b266775af728c2dc.tar.gz | |
["lint", "targets"]: deduplicate tasks
In case many "targets" are given, the field "lint" will contain
all the concatenation of the provider "lint" of the given targets.
There is, however, not need to lint the same file in the same
context twice, so deduplicate the targets first. While this does
not change the amount of lint actions carried out (as equal actions
are handled only once anyway), it keeps the summary clean by not
having dulicate entries.
| -rw-r--r-- | rules/lint/RULES | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/rules/lint/RULES b/rules/lint/RULES index d7b27030..7e2861c7 100644 --- a/rules/lint/RULES +++ b/rules/lint/RULES @@ -133,6 +133,9 @@ } } ] + , [ "lint results" + , {"type": "nub_right", "$1": {"type": "var", "name": "lint results"}} + ] , [ "summary input" , {"type": "enumerate", "$1": {"type": "var", "name": "lint results"}} ] |