ARMmbed
/
mbed-os
mirror of https://github.com/ARMmbed/mbed-os.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Fixes toolchain filtering

pull/1502/head
Brian Daniels 2016-01-12 15:34:02 -06:00
parent 26e3c61983
commit bd8fcebfde
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
workspace_tools/build_release.py
View File

@ -177,7 +177,7 @@ if __name__ == '__main__':
if options.toolchains:
print "Only building using the following toolchains: %s" % (options.toolchains)
toolchainSet = set(toolchains)
toolchains = toolchainSet and set((options.toolchains).split(','))
toolchains = toolchainSet.intersection(set((options.toolchains).split(',')))
for toolchain in toolchains:
id = "%s::%s" % (target_name, toolchain)