diff options
| author | Eric Engestrom <[email protected]> | 2019-08-03 18:21:26 +0100 |
|---|---|---|
| committer | Eric Engestrom <[email protected]> | 2019-08-04 11:06:27 +0100 |
| commit | 59f8809f3c696fc60c4447341702ca8a7bf557a5 (patch) | |
| tree | 6eb967a4128989e99394aa43ac1c42730f828c81 /bin | |
| parent | 81b3d141b37f37ed883e6b06a7980bcee761d604 (diff) | |
symbols-check: discard platform symbols early
(as the comment there already claimed)
Signed-off-by: Eric Engestrom <[email protected]>
Tested-by: Vinson Lee <[email protected]>
Diffstat (limited to 'bin')
| -rw-r--r-- | bin/symbols-check.py | 4 |
1 files changed, 2 insertions, 2 deletions
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 = [ |