diff --git a/bin/symbols-check.py b/bin/symbols-check.py index 7b1a086e95f..39ad1451852 100644 --- a/bin/symbols-check.py +++ b/bin/symbols-check.py @@ -27,6 +27,8 @@ def get_symbols(nm, lib): stderr=open(os.devnull, 'w')).decode("ascii") for line in output.splitlines(): (_, _, symbol_name) = line.split() + if symbol_name in PLATFORM_SYMBOLS: + continue symbols.append(symbol_name) return symbols @@ -97,8 +99,6 @@ def main(): continue if symbol in optional_symbols: continue - if symbol in PLATFORM_SYMBOLS: - continue unknown_symbols.append(symbol) missing_symbols = [