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

If custom_targets_directory exists use it over source_dir

pull/9401/head
Garrett 2019-01-16 12:17:26 -05:00 committed by Garrett LoVerde
parent 83d679ae38
commit 31615eb542
1 changed files with 5 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
tools/options.py
View File

@ -123,7 +123,11 @@ def extract_profile(parser, options, toolchain, fallback="develop"):
def extract_mcus(parser, options):
try:
if options.source_dir:
if options.custom_targets_directory:
for custom_targets_directory in options.custom_targets_directory:
Target.add_extra_targets(custom_targets_directory)
update_target_data()
elif options.source_dir:
for source_dir in options.source_dir:
Target.add_extra_targets(source_dir)
update_target_data()