+ logdata=`git log --color "$base".."$ref"`
+ diffdata=`git diff --color --find-copies-harder --ignore-space-change "$base"..."$ref"`
+ if [ -z "$logdata" ]; then
+ reportecho4 "--> not merging, no changes vs master"
+ elif [ -z "$diffdata" ]; then
+ reportecho4 "--> not merging, no changes vs master, branch contains redundant history"
+ if yesno "Branch \"$ref\" probably should get deleted. Do it?" '{ echo "$logdata"; } | less -r'; then
+ git push origin :"${ref#refs/remotes/origin/}"
+ reportecho4 "--> branch deleted"
+ fi
+ elif [ -n "$note" ]; then