From 2df55f5c3522e52bf6444ed561667ef42c2d0d25 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.
---
 lint/RULES | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/lint/RULES b/lint/RULES
index d7b2703..7e2861c 100644
--- a/lint/RULES
+++ b/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