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

Merge pull request #8248 from theotherjimmy/fix-7954 

Tools, Resources: Convert to a set during win2unix
pull/8253/merge
Cruz Monrreal 2018-10-11 10:36:52 -05:00 committed by GitHub
parent 3568c54da6 f6310a00c3
commit 19190d62d2
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
tools/resources/__init__.py
View File

@ -189,7 +189,7 @@ class Resources(object):
for file_type in self.ALL_FILE_TYPES:
v = [f._replace(name=f.name.replace(sep, self._sep)) for
f in self.get_file_refs(file_type)]
self._file_refs[file_type] = v
self._file_refs[file_type] = set(v)
def __str__(self):
s = []