| Index: runtime/tools/create_resources.py
|
| diff --git a/runtime/tools/create_resources.py b/runtime/tools/create_resources.py
|
| index 32ffdb1a183996ff0b9036b23b10cd916e57b3db..b4f7fa8d4a5ce044f546d86ae6a2a8816e403196 100644
|
| --- a/runtime/tools/create_resources.py
|
| +++ b/runtime/tools/create_resources.py
|
| @@ -127,6 +127,9 @@ def main(args):
|
| src_path = os.path.join(dirname, f)
|
| if (os.path.isdir(src_path)):
|
| continue
|
| + # Skip devtools version
|
| + if (src_path.find("index_devtools") != -1):
|
| + continue
|
| files.append(src_path)
|
|
|
| for arg in args:
|
| @@ -145,4 +148,4 @@ def main(args):
|
| return -1
|
|
|
| if __name__ == '__main__':
|
| - sys.exit(main(sys.argv))
|
| + sys.exit(main(sys.argv))
|
|
|