Merge branch 'master' into master

This commit is contained in:
Gennadiy Civil 2018-03-22 12:56:01 -04:00 committed by GitHub
commit a1692ed133
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23

View File

@ -87,7 +87,7 @@ test_script:
if ($env:generator -eq "MinGW Makefiles") {
return # No test available for MinGW
}
& ctest -C $env:configuration --timeout 300 --output-on-failure
& ctest -C $env:configuration --timeout 600 --output-on-failure
if ($LastExitCode -ne 0) {
throw "Exec: $ErrorMessage"
}