diff options
author | 2015-09-04 15:17:12 -0700 | |
---|---|---|
committer | 2015-09-25 11:15:04 -0700 | |
commit | 3ef8c0862e8cc71b8d8d8420117537d6f6e6f3fc (patch) | |
tree | b5dc3d911ce2f9603ed36e41b1d2e15fb95ac587 /tools | |
parent | ff60024eaf67dea0faf899f80c099460d87fa3ad (diff) |
More PDB trickery
Diffstat (limited to 'tools')
-rwxr-xr-x | tools/run_tests/run_tests.py | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/run_tests/run_tests.py b/tools/run_tests/run_tests.py index d271137ca1..ac5eef663e 100755 --- a/tools/run_tests/run_tests.py +++ b/tools/run_tests/run_tests.py @@ -617,7 +617,7 @@ if platform.system() == 'Windows': # better do parallel compilation extra_args.extend(["/m"]) # disable PDB generation: it's broken, and we don't need it during CI - extra_args.extend(["/p:GenerateDebugInformation=false", "/p:DebugInformationFormat=None"]) + extra_args.extend(["/p:Jenkins=true"]) return [ jobset.JobSpec(['vsprojects\\build.bat', 'vsprojects\\%s.sln' % target, |