ppush: prefer pushurl

If remote has been configured with separate pushurl, try that first.

Change-Id: I764ed5c4355da54ea0a737aec7feb7048fb5df66
Reviewed-by: Oswald Buddenhagen <oswald.buddenhagen@gmx.de>
Reviewed-by: Tor Arne Vestbø <tor.arne.vestbo@qt.io>
Reviewed-by: Edward Welbourne <edward.welbourne@qt.io>

1 files changed, 5 insertions, 1 deletions

diff --git a/bin/git-ppush b/bin/git-ppush
index 90b58a3..ef0ecd5 100755
--- a/bin/git-ppush
+++ b/bin/git-ppush
@@ -189,7 +189,11 @@ sub run_setup
             die "Have no upstream. Cannot determine base remote.\n" if (!$base);
             chomp $base;
         }
-        $url = `git config remote.$base.url`;
+        # Personal repos can only be in Gerrit, but the base repo might be using
+        # a mirror. Try the pushurl first, if that has been set up, it most likely
+        # will point to Gerrit. It will be set as .url, so both push and fetch work.
+        $url = `git config remote.$base.pushurl`;
+        $url = `git config remote.$base.url` if (!$url);
         die "Cannot determine URL of base remote. Try --url.\n" if (!$url);
         chomp $url;
     }