[CI] Cancel previous build if new commit has been pushed to a PR (#6518)
authorTianqi Chen <tqchen@users.noreply.github.com>
Mon, 21 Sep 2020 00:49:23 +0000 (17:49 -0700)
committerGitHub <noreply@github.com>
Mon, 21 Sep 2020 00:49:23 +0000 (17:49 -0700)
commitb4f8b287333f9379ac24c07789bd6171a4e4e1ca
tree9f5145503888b528f9591bcdaf53c72b2b4657e3
parentb926f79537e7431ff7bb4602dff3164f8491e97b
[CI] Cancel previous build if new commit has been pushed to a PR (#6518)
Jenkinsfile