Hopefully speed up Jenkins builds
diff --git a/tools/run_tests/run_tests.py b/tools/run_tests/run_tests.py
index 234e13b..1f1e7da 100755
--- a/tools/run_tests/run_tests.py
+++ b/tools/run_tests/run_tests.py
@@ -477,10 +477,14 @@
if platform.system() == 'Windows':
def make_jobspec(cfg, targets):
+ extra_args = []
+ if args.travis:
+ extra_args.extend(["/m", "/p:DebugSymbols=false", "/p:DebugType=None"])
return [
jobset.JobSpec(['vsprojects\\build.bat',
'vsprojects\\%s.sln' % target,
- '/p:Configuration=%s' % _WINDOWS_CONFIG[cfg]],
+ '/p:Configuration=%s' % _WINDOWS_CONFIG[cfg]] +
+ extra_args,
shell=True, timeout_seconds=90*60)
for target in targets]
else: