We need a `git pull` after switching to the master branch, to make sure we see
authorWard Vandewege <ward@curii.com>
Wed, 19 Aug 2020 23:43:27 +0000 (19:43 -0400)
committerWard Vandewege <ward@curii.com>
Wed, 19 Aug 2020 23:43:27 +0000 (19:43 -0400)
commit4197c8b8bf40d546271ea91e42b950aa33d48a11
tree1e1a8c2e5f815c7844ed6b160076fac941a638cf
parentac0a28165e30c658931126aa92262aee32c52691
We need a `git pull` after switching to the master branch, to make sure we see
the complete lists of branches.

No issue #

Arvados-DCO-1.1-Signed-off-by: Ward Vandewege <ward@curii.com>
jenkins/run-delete-merged-branches.sh