From ceb8f9f5549d7bb8a6812ede6ff9dd79f79a491e Mon Sep 17 00:00:00 2001
From: Baris Metin <Talip-Baris.Metin@sophia.inria.fr>
Date: Fri, 18 Jun 2010 15:19:50 +0200
Subject: [PATCH] fetch tags and pull from local master before pushing for
 merges

---
 scripts/git-mirror.sh | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)
 mode change 100644 => 100755 scripts/git-mirror.sh

diff --git a/scripts/git-mirror.sh b/scripts/git-mirror.sh
old mode 100644
new mode 100755
index 434b7e8..5dbc411
--- a/scripts/git-mirror.sh
+++ b/scripts/git-mirror.sh
@@ -14,7 +14,7 @@ function mirror () {
         then
 	    echo "xxxxxxxxxxxxxxxxxxxxxxxxxxxxxx pulling from ${REPO_NAME}"
             pushd ${REPO}
-            git pull --tags
+            git fetch --tags
             git pull
             popd
         else
@@ -27,6 +27,9 @@ function mirror () {
 
         echo "xxxxxxxxxxxxxxxxxxxxxxxxxxxxxx pushing ${REPO_NAME} to local master"
         pushd ${REPO}
+        git fetch local_master --tags
+        git pull local_master
+            
         git push local_master
         git push --tags local_master
         popd
-- 
2.47.0