commit e01ed36e25fa4647eb5adda1f46706c4fd07235d
author Jin <jin@users.noreply.github.com> Mon Aug 10 17:18:13 2020 +0800
committer GitHub <noreply@github.com> Mon Aug 10 11:18:13 2020 +0200
tree 03becc5b2125831312b200ce51239ed088818bbb
parent 8f41b2596923b1b5cbf865fc794366897d190aa0

Extend gitsync to mirror specific branches. (#1016)

Tulsi is now published to an 'upstream' branch, not 'master'. This PR extends the gitsync script to support mirroring non-master branches.

gitsync/gitsync.sh

diff --git a/gitsync/gitsync.sh b/gitsync/gitsync.sh
index b09e139..da4212f 100755
--- a/gitsync/gitsync.sh
+++ b/gitsync/gitsync.sh
@@ -22,8 +22,8 @@
 # where
 #   direction can be ==> or <=>
 REPOSITORIES=(
-    "https://bazel.googlesource.com/bazel ==> git@github.com:bazelbuild/bazel.git bazel"
-    "https://bazel.googlesource.com/tulsi ==> git@github.com:bazelbuild/tulsi.git tulsi"
+    "https://bazel.googlesource.com/bazel ==> git@github.com:bazelbuild/bazel.git bazel master"
+    "https://bazel.googlesource.com/tulsi ==> git@github.com:bazelbuild/tulsi.git tulsi upstream"
 )
 
 set -euxo pipefail
@@ -57,16 +57,17 @@
   local direction="$2"
   local destination="$3"
   local name="$4"
+  local branch="$5"
 
   pushd "${name}"
-  echo "Syncing ${origin} ${direction} ${destination} ..."
+  echo "Syncing ${origin} ${direction} ${destination} on the $branch branch..."
   git remote update --prune
-  git checkout "origin/master" -B "master"
+  git checkout "origin/$branch" -B "$branch"
   if [[ "${direction}" == "<=>" ]]; then
-    git rebase "destination/master"
-    git push -f origin master
+    git rebase "destination/$branch"
+    git push -f origin "$branch"
   fi
-  git push destination master
+  git push destination "$branch"
   popd
 }