diff options
Diffstat (limited to 'dev/run-tests-jenkins')
| -rwxr-xr-x | dev/run-tests-jenkins | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/dev/run-tests-jenkins b/dev/run-tests-jenkins index 8b2a44fd72..f452ab66ef 100755 --- a/dev/run-tests-jenkins +++ b/dev/run-tests-jenkins @@ -185,8 +185,6 @@ done # run tests { - # Marks this build is a pull request build. - export AMP_JENKINS_PRB=true timeout "${TESTS_TIMEOUT}" ./dev/run-tests test_result="$?" |