3 MIRROR_GIT="git://git.planet-lab.org"
5 LOCAL_MIRROR_DIR="/git-mirror"
11 echo "xxxxxxxxxxxxxxxxxxxxxxxxxxxxxx $1"
16 echo "[ERROR] xxxxxxxxxxxxxxxxxxxxxxxxxxxxxx $1"
22 COMMAND="$1 &> /dev/null"
29 pushd ${REPO} > /dev/null
36 NAME=$(basename ${arg} | sed s/.git$//g)
38 REPO_DIR=${LOCAL_MIRROR_DIR}/${NAME}
39 MIRROR_REPO=${MIRROR_GIT}/${GIT_NAME}
40 MASTER_REPO=${MASTER_GIT}/${GIT_NAME}
42 # if there is no remote repository it may be that we only have
43 # the repository locally and don't need to mirror
44 git ls-remote $MIRROR_REPO &> /dev/null
49 msg "pulling from ${NAME}"
50 run "git fetch origin --tags" ${REPO_DIR}
51 run "git fetch origin" ${REPO_DIR}
52 run "git merge --ff origin/master" ${REPO_DIR}
55 error "Can not fetch from ${MASTER_REPO}"
58 msg "mirroring ${NAME} for the first time"
59 run "git clone ${MIRROR_REPO}" ${LOCAL_MIRROR_DIR}
60 run "git remote add local_master ${MASTER_REPO}" ${REPO_DIR}
63 msg "pushing ${NAME} to local master"
64 run "git fetch local_master --tags" ${REPO_DIR}
65 run "git fetch local_master" ${REPO_DIR}
66 run "git merge --ff local_master/master" ${REPO_DIR}
69 error "Can not fetch from ${MIRROR_REPO}"
71 run "git push local_master" ${REPO_DIR}
72 run "git push --tags local_master" ${REPO_DIR}
79 while getopts ":hq" opt
87 echo "USAGE: $0 [-q] REPONAME*"
91 echo "Invalid option: -$OPTARG" >&2