wrong name

[infrastructure.git] / scripts / git-mirror.sh

diff --git a/scripts/git-mirror.sh b/scripts/git-mirror.sh
index 1f2a5b9..8761ac1 100755 (executable)
--- a/scripts/git-mirror.sh
+++ b/scripts/git-mirror.sh
@@ -2,7 +2,7 @@
 COMMAND=$(basename $0)
 
 # for sending emails (-a option)
-ADMINS="Thierry.Parmentelat@inria.fr baris@metin.org"
+ADMINS="Thierry.Parmentelat@inria.fr"
 # the other end of the mirror (-r option)
 REMOTE_GIT="git://git.planet-lab.org"
 # options
@@ -144,6 +144,10 @@ function mirror_repo () {
     REMOTE_REPO=${REMOTE_GIT}/${GIT_NAME}
     MASTER_REPO=${MASTER_GIT}/${GIT_NAME}
 
+    # if the local master is a symlink (like /git/vserver-reference.git -> sliceref.git) 
+    # then skip it, the target itself will be handled if in scope
+    [ -h ${MASTER_REPO} ] && return
+
     # if there is no remote repository it may be that we only have
     # the repository locally and don't need to mirror
     git ls-remote $REMOTE_REPO &> /dev/null || return
@@ -191,6 +195,8 @@ function mirror_repo () {
     fi
     # success, remove previous check file if any
     clear_notify $REPO_DIR
+    # touch a stamp so it's easier to figure out where/if things get stuck
+    touch ${REPO_DIR}/MIRRORED.stamp
 }
 
 function usage () {