try to handle the case if the branch has been remotely deleted in "push"

diff --git a/all b/all
index 729cce2297c447736e9abfa44f9972c1239a26c5..09292ee0d19a0cf22d8e25041925523fa6247814 100755 (executable)
--- a/all
+++ b/all
@@ -331,7 +331,7 @@ case "$cmd" in
                                fi
                        fi
                        rem=`git config "branch.$r.remote" || echo origin`
                                fi
                        fi
                        rem=`git config "branch.$r.remote" || echo origin`

-                       if git log "$rem/$r".."$r" | grep .; then
+                       if { git log "$rem/$r".."$r" || git log origin/master.."$r"; } | grep .; then

                                a=
                                while [ x"$a" != x"y" -a x"$a" != x"n" ]; do
                                        echo "Push \"$r\" in $dv?"
                                a=
                                while [ x"$a" != x"y" -a x"$a" != x"n" ]; do
                                        echo "Push \"$r\" in $dv?"