push to remote servers

diff --git a/scripts/git/post-receive b/scripts/git/post-receive
index 6b99428b7c9784d1475576dbc69d5ab2f3e93c41..ac9d073a5141ac3fbb658748676a640c4939a9c9 100755 (executable)
--- a/scripts/git/post-receive
+++ b/scripts/git/post-receive
@@ -24,6 +24,12 @@ GIT_EXEC='env -i git'
 # Abort if there are local untracked files
 ABORT_UNTRACKED=true
 
+# Push changes to any remotes we have configured
+PUSH_TO_REMOTES=false
+
+# The remote branch to push to
+PUSH_TO_BRANCH='master'
+
 while read oldrev newrev refname
 do
 :
@@ -131,4 +137,11 @@ else
        $GIT_EXEC tag -f $STABLE_TAG $newrev
 fi
 
+if [ $PUSH_TO_REMOTES ]; then
+        echo "Pushing to remote servers"
+        for remote in `$GIT_EXEC remote`; do
+                $GIT_EXEC push "$remote" "$PUSH_TO_BRANCH"
+        done
+fi
+
 exit 0