From c5d844c7c3d6f2ec8941e7b3b266775af728c2dc Mon Sep 17 00:00:00 2001
From: Klaus Aehlig <klaus.aehlig@huawei.com>
Date: Wed, 14 Aug 2024 16:18:55 +0200
Subject: ["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.
---
 rules/lint/RULES | 3 +++
 1 file changed, 3 insertions(+)

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"}}
         ]
-- 
cgit v1.2.3