Merge pull request #3068 from ctiller/make-might-take-a-very-long-time
Windows builds need longer
diff --git a/tools/run_tests/run_tests.py b/tools/run_tests/run_tests.py
index beb4343..beb8805 100755
--- a/tools/run_tests/run_tests.py
+++ b/tools/run_tests/run_tests.py
@@ -465,7 +465,8 @@
if platform.system() == 'Windows':
def make_jobspec(cfg, targets):
return jobset.JobSpec(['make.bat', 'CONFIG=%s' % cfg] + targets,
- cwd='vsprojects', shell=True)
+ cwd='vsprojects', shell=True,
+ timeout_seconds=30*60)
else:
def make_jobspec(cfg, targets):
return jobset.JobSpec([os.getenv('MAKE', 'make'),