diff options
Diffstat (limited to 'scripts/list-workarounds')
| -rwxr-xr-x | scripts/list-workarounds | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/scripts/list-workarounds b/scripts/list-workarounds index 7bfd82dd..6c8c636a 100755 --- a/scripts/list-workarounds +++ b/scripts/list-workarounds @@ -47,7 +47,10 @@ def parse(me): platforms = match.group('platforms') if wa_name in workarounds: - workarounds[wa_name] += parse_platforms(platforms) + platforms = parse_platforms(platforms) + for p in platforms: + if not p in workarounds[wa_name]: + workarounds[wa_name].append(p) else: workarounds[wa_name] = parse_platforms(platforms) |