diff options
| -rwxr-xr-x | configure.py | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/configure.py b/configure.py index 4a1c679..d861c24 100755 --- a/configure.py +++ b/configure.py @@ -141,6 +141,14 @@ for target in targets: for libdir in libdirs: subdir_list_file = os.path.join(libdir, 'SOURCES') manifest_deps.add(subdir_list_file) + override_list_file = os.path.join(libdir, 'OVERRIDES') + + # Add target overrides + if os.path.exists(override_list_file): + for override in open(override_list_file).readlines(): + override = override.rstrip() + sources_seen.add(override) + for src in open(subdir_list_file).readlines(): src = src.rstrip() if src not in sources_seen: |