diff options
Diffstat (limited to 'scripts/internal/generate_manifest.py')
-rwxr-xr-x | scripts/internal/generate_manifest.py | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/scripts/internal/generate_manifest.py b/scripts/internal/generate_manifest.py index 3d3e83b0..b7ad8c7e 100755 --- a/scripts/internal/generate_manifest.py +++ b/scripts/internal/generate_manifest.py @@ -23,16 +23,15 @@ def sh(cmd): def main(): - files = [] + files = set() for file in sh("git ls-files").split('\n'): if file.startswith(SKIP_PREFIXES) or \ os.path.splitext(file)[1].lower() in SKIP_EXTS or \ file in SKIP_FILES: continue - if file not in files: - files.append(file) + files.add(file) - for file in files: + for file in sorted(files): print("include " + file) |