[ARVADOS-DEV] updated: 8a1d756a02b0734c95b6ae1a0a99ea8374dcacbe

[Git user]

Summary of changes:
 jenkins/run-delete-merged-branches.sh | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

       via  8a1d756a02b0734c95b6ae1a0a99ea8374dcacbe (commit)
      from  9b40808f26dc7d548a80b6bfa1d726401695779e (commit)

Those revisions listed above that are new to this repository have
not appeared on any other notification email; so we list those
revisions in full, below.


commit 8a1d756a02b0734c95b6ae1a0a99ea8374dcacbe
Author: Javier Bértoli <javier at curoverse.com>
Date:   Thu Mar 30 18:27:07 2017 -0300

    Make delete script a little more verbose. Update remote branches before deleting
    
    refs #11020

diff --git a/jenkins/run-delete-merged-branches.sh b/jenkins/run-delete-merged-branches.sh
index f1dc2ef..175b144 100755
--- a/jenkins/run-delete-merged-branches.sh
+++ b/jenkins/run-delete-merged-branches.sh
@@ -1,4 +1,4 @@
-#!/usr/bin/env bash
+#!/bin/bash -x
 
 # Copyright (C) The Arvados Authors. All rights reserved.
 #
@@ -22,6 +22,7 @@ trap '_exit_handler $LINENO' EXIT ERR
 # IE: "keep_this_branch|also_this_other|and_this_one"
 branches_to_keep="master"
 
+git remote update --prune
 git checkout master
 
 git branch --remote --merged | \

-----------------------------------------------------------------------


hooks/post-receive
--