Don't fix headers in /build

2026-09-01 03:11:09 +00:00 · 2013-08-22 10:22:07 +02:00
parent 1c993d3a5f
commit f2de1fbfcc
1 changed files with 2 additions and 0 deletions
@@ -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)