scripts/git: Add TOR_EXTRA_REMOTE_* for an extra git remote

When running git-setup-dirs.sh.

Part of 32347.
This commit is contained in:
teor 2019-10-31 14:28:27 +10:00
parent 38e8cca6a1
commit 1ffb3b549f
No known key found for this signature in database
GPG Key ID: 10FEAA0E7075672A

View File

@ -42,6 +42,14 @@ function usage()
echo " (current: $GITHUB_PUSH)"
echo " TOR_EXTRA_CLONE_ARGS: extra arguments to git clone"
echo " (current: $TOR_EXTRA_CLONE_ARGS)"
echo " TOR_EXTRA_REMOTE_NAME: the name of an extra remote"
echo " This remote is not pulled by this script or git-pull-all.sh."
echo " This remote is not pushed by git-push-all.sh."
echo " (current: $TOR_EXTRA_REMOTE_NAME)"
echo " TOR_EXTRA_REMOTE_PULL: the extra remote pull URL."
echo " (current: $TOR_EXTRA_REMOTE_PULL)"
echo " TOR_EXTRA_REMOTE_PUSH: the extra remote push URL"
echo " (current: $TOR_EXTRA_REMOTE_PUSH)"
echo " we recommend that you set these env vars in your ~/.profile"
}
@ -510,6 +518,17 @@ set_tor_github_pr_fetch_config
# Now fetch them all
fetch_remote "tor-github"
# Extra remote
if [ "$TOR_EXTRA_REMOTE_NAME" ]; then
printf "%s Setting up remote %s\\n" "$MARKER" \
"${BYEL}$TOR_EXTRA_REMOTE_NAME${CNRM}"
# Add remote
add_remote "$TOR_EXTRA_REMOTE_NAME" "$TOR_EXTRA_REMOTE_PULL"
set_remote_push "$TOR_EXTRA_REMOTE_NAME" "$TOR_EXTRA_REMOTE_PUSH"
# But leave it to the user to decide if they want to fetch it
#fetch_remote "$TOR_EXTRA_REMOTE_NAME"
fi
# Go over all configured worktree.
for ((i=0; i<COUNT; i++)); do
branch=${!WORKTREE[$i]:0:1}