From f8a80a8258af86cb1e87f763c7ef1734b06e2c22 Mon Sep 17 00:00:00 2001 From: Mikko Rasa Date: Sun, 16 Jul 2023 12:45:53 +0300 Subject: [PATCH] Avoid duplicate things when generating OpenGL extensions --- scripts/extgen.py | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/scripts/extgen.py b/scripts/extgen.py index 9c859c33..9faec3e9 100755 --- a/scripts/extgen.py +++ b/scripts/extgen.py @@ -770,10 +770,12 @@ def get_extension(api_map, ext_name): def resolve_things(api, things): rthings = [] for t in things: - ct = [api.core_things[a] for a in t.aliases if a in api.core_things] - if ct: - rthings += ct - else: + cthings = [api.core_things[a] for a in t.aliases if a in api.core_things] + if cthings: + for c in cthings: + if c not in rthings: + rthings.append(c) + elif t not in rthings: rthings.append(t) return rthings -- 2.45.2