From d3b447c20368dab68636e79b893547757fdab8df Mon Sep 17 00:00:00 2001
From: chriseth <chris@ethereum.org>
Date: Wed, 12 Jul 2017 19:06:04 +0200
Subject: [PATCH] Ignore the docs build directory.

---
 scripts/isolate_tests.py | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/scripts/isolate_tests.py b/scripts/isolate_tests.py
index d075b07f3..cfaef2106 100755
--- a/scripts/isolate_tests.py
+++ b/scripts/isolate_tests.py
@@ -83,7 +83,9 @@ if __name__ == '__main__':
     if len(sys.argv) > 2 and sys.argv[2] == 'docs':
       docs = True
 
-    for root, dir, files in os.walk(path):
+    for root, subdirs, files in os.walk(path):
+        if '_build' in subdirs:
+          subdirs.remove('_build')
         for f in files:
             path = join(root, f)
             if docs: