[PATCH 1/2] release.sh: allow changing the git remote's name

[Julien Cristau]

---
I'm using origin for git.debian.org, and upstream for git.fd.o, so this
makes it possible to push releases to the right place :)

 release.sh |   11 +++++++++--
 1 files changed, 9 insertions(+), 2 deletions(-)

diff --git a/release.sh b/release.sh
index 9f7358d..f6eaf23 100755
--- a/release.sh
+++ b/release.sh
@@ -9,6 +9,7 @@ host_people=annarchy.freedesktop.org
 host_xorg=xorg.freedesktop.org
 host_dri=dri.freedesktop.org
 user=`whoami`
+remote=origin
 
 usage()
 {
@@ -19,6 +20,7 @@ Options:
   --force       force overwritting an existing release
   --user <name> username on $host_people (default "`whoami`")
   --help        this help message
+  --remote      git remote where the change should be pushed (default "origin")
 HELP
 }
 
@@ -81,6 +83,11 @@ while [ $# != 0 ]; do
 	user=$1
 	shift
 	;;
+    --remote)
+        shift
+        remote=$1
+        shift
+        ;;
     --*)
         echo "error: unknown option"
         usage
@@ -171,6 +178,6 @@ echo "installing release into server"
 scp $tarball_dir/$targz $tarball_dir/$tarbz2 $user@$host_people:$srv_path
 
 echo "pushing changes upstream"
-git push origin
-git push origin $tag_current
+git push $remote
+git push $remote $tag_current
 
-- 
1.6.3.3