diff --git a/scripts/fix_headers.py b/scripts/fix_headers.py index d578acd4..3439c6f1 100755 --- a/scripts/fix_headers.py +++ b/scripts/fix_headers.py @@ -132,6 +132,8 @@ def findHeadersAndFiles(): dirs.remove(".git") if "developer.github.com" in dirs: dirs.remove("developer.github.com") + if "build" in dirs: + dirs.remove("build") for filename in files: fullname = os.path.join(root, filename)